From First-Order Theories to Logic Programs
Heng Zhang, Yan Zhang and Yi Zhou
This paper focuses on computing first-order theories under stable model semantics and circumscription. A reduction from arbitrary first-order theories to logic programs under stable model semantics over finite structures is proposed, and an embedding of circumscription into stable model semantics is also found. Having such reduction and embedding, the reasoning problems represented by first-order theories under both semantics can then be handled by using existing answer set solvers. The effectiveness of this approach in computing some hard problems beyond NP is demonstrated by some experiments.