Discovering Classes of Strongly Equivalent Logic Programs

We report on a successful experiment of computeraided theorem discovery in the area of logic programming with answer set semantics. Specifically, with the help of computers, we discovered exact conditions that capture the strong equivalence between a set of a rule and the empty set, a set of a rule and another set of a rule, a set S of two rules and a subset of S with one rule, a set of two rules and a set of another rule, and a set S of three rules and a subset of S with two rules. We prove some general theorems that can help us verify the correctness of these conditions, and discuss the usefulness of our results in program simplification.

• Type: Journal
• Year: 2007
• Where: JAIR
• Authors: Fangzhen Lin, Yin Chen
• Keywords: Answer Set Semantics, Exact Conditions, JAIR 2007, Strong Equivalence