Computing Answer Sets Using Model Generation Theorem Provers

Sabuncu, Orkunt
Alpaslan, Ferda Nur
Model generation theorem provers have the capability of producing a model when the first-order input theory is satisfiable. Because grounding step may generate huge propositional instances of the program it hardens the search process of answer set solvers. We propose the use of model generation theorem provers as computational engines for Answer Set Programming (ASP). It can be seen as lifting of SAT-based ASP to the first-order level for tight programs to eliminate the grounding step of ASP or do it more intelligently.
Citation Formats
O. Sabuncu and F. N. Alpaslan, “Computing Answer Sets Using Model Generation Theorem Provers,” presented at the 4th International Workshop on Answer Set Programming, 2007, 2007, Accessed: 00, 2021. [Online]. Available: