Discovering Classes of Strongly Equivalent Logic Programs

Abstract

In this paper we apply computer-aided theorem discovery technique to discover theorems about strongly equivalent logic programs under the answer set semantics. Our discovered theorems capture new classes of strongly equivalent logic programs that can lead to new program simplification rules that preserve strong equivalence. Specifically, with the help of computers, we discovered exact conditions that capture the strong equivalence between a rule and the empty set, between two rules, between two rules and one of the two rules, between two rules and another rule, and between three rules and two of the three rules.

References in corpus (3)

• The DLV System for Knowledge Representation and Reasoning
• Smodels: A System for Answer Set Programming
• Discovering Classes of Strongly Equivalent Logic Programs

Cited by in corpus (7)

• Discovering Classes of Strongly Equivalent Logic Programs
• Epistemic Logic Programs: A Different World View
• On Uniform Equivalence of Epistemic Logic Programs
• On the Strong Equivalences of LPMLN Programs
• On the Strong Equivalences for LPMLN Programs
• A Syntactic Approach to Studying Strongly Equivalent Logic Programs
• Strong Equivalence for Epistemic Logic Programs Made Easy (Extended Version)