| Home > Publications > Reports > Informatics (CW) |
CW 426
Maarten Mariën, Rudradeb Mitra, Marc Denecker, Maurice Bruynooghe
Satisfiability checking for PC(ID)
Abstract
The logic FO(ID) is an extension of classical first order logic with inductive definitions. This paper studies the satisifiability problem for PC(ID), the propositional fragment of FO(ID). We develop a theoretical 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.
report.pdf (222K) / mailto: M. Mariën