Abstract:
The logic FO(ID) extends classical first order logic with inductive definitions. This paper studies the satisifiability problem for PC(ID), its propositional 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.
Published: M. Mariën, R. Mitra, M. Denecker, en M. Bruynooghe, Satisfiability checking for PC(ID), Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005, Proceedings (Sutcliffe, G. and Voronkov, A., eds.), vol 3835, Lecture Notes in Computer Science, pp. 565-579, 2005