Abstract
The logic FO(ID) extends classical first order logic with inductive definitions. This paper studies the satisifiability problem for PC(ID), its prepositional fragment. We develop a framework for model generation in this logic, present an algorithm and prove its correctness. As FO(ID) is an integration of classical logic and logic programming, our algorithm integrates techniques from SAT and ASP. We report on a prototype system, called MIDL, experimentally validating our approach. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Mariën, M., Mitra, R., Denecker, M., & Bruynooghe, M. (2005). Satisfiability checking for PC(ID). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3835 LNAI, pp. 565–579). Springer Verlag. https://doi.org/10.1007/11591191_39
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
