Discovering Classes of Strongly Equivalent Logic Programs

TL;DR

This paper uses computer-aided theorem discovery to identify new classes of strongly equivalent logic programs under answer set semantics, enabling better program simplification rules.

Contribution

It introduces a novel computer-assisted method to discover exact conditions for strong equivalence among logic programs, expanding theoretical understanding.

Findings

Discovered conditions for strong equivalence between a rule and the empty set

Identified equivalence conditions between pairs and triples of rules

Proposed new program simplification rules based on these theorems

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.