2015/07/01 by Bart Bogaerts, BART BOGAERTS, Guy Van den Broeck +1
Computer Science · #Autoepistemic logic #Constructive #Default logic #Fixed point #Logic program #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Modal μ-calculus #Preprocessor #Propositional calculus #Semantic Web and Ontologies #Semantics (computer science) #cs.LO
paper · pdf · doi:10.1017/s1471068415000162
published as Theory and Practice of Logic Programming 15 (2015) 464-480
openalex publication_date 2015/07/01 · arxiv created 2015/07/23 · openalex created_date 2016/06/24 · arxiv updated 2020/02/19 · openalex updated_date 2026/08/05
Abstract Recent advances in knowledge compilation introduced techniques to compile positive logic programs into propositional logic, essentially exploiting the constructive nature of the least fixpoint computation. This approach has several advantages over existing approaches: it maintains logical equivalence, does not require (expensive) loop-breaking preprocessing or the introduction of auxiliary variables, and significantly outperforms existing algorithms. Unfortunately, this technique is limited to negation-free programs. In this paper, we show how to extend it to general logic programs under the well-founded semantics. We develop our work in approximation fixpoint theory, an algebraical framework that unifies semantics of different logics. As such, our algebraical results are also applicable to autoepistemic logic, default logic and abstract dialectical frameworks.