Counterexample guided abstraction refinement algorithm for propositional circumscription

DOI10.1007/978-3-642-15675-5_18MaRDI QIDQ4930765zbMATH OpenOpenAlexFDO

Authors Mikoláš Janota, Radu Grigore, Joao Marques-Silva

Publication date 1 October 2010

Published in Logics in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1006.5896

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Abstract: Circumscription is a representative example of a nonmonotonic reasoning inference technique. Circumscription has often been studied for first order theories, but its propositional version has also been the subject of extensive research, having been shown equivalent to extended closed world assumption (ECWA). Moreover, entailment in propositional circumscription is a well-known example of a decision problem in the second level of the polynomial hierarchy. This paper proposes a new Boolean Satisfiability (SAT)-based algorithm for entailment in propositional circumscription that explores the relationship of propositional circumscription to minimal models. The new algorithm is inspired by ideas commonly used in SAT-based model checking, namely counterexample guided abstraction refinement. In addition, the new algorithm is refined to compute the theory closure for generalized close world assumption (GCWA). Experimental results show that the new algorithm can solve problem instances that other solutions are unable to solve.

Recommendations

• An algorithm to compute circumscription
• The complexity of propositional closed world reasoning and circumscription
• Propositional circumscription and extended closed-world reasoning are \(\Pi_ 2^ P\)-complete
• On compact representations of propositional circumscription
• Revisiting grounded circumscription in description logics

Cited in

(9)

• An algorithm to compute circumscription
• Solving QBF with counterexample guided refinement
• Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem
• Abstraction-based algorithm for 2QBF
• Model enumeration in propositional circumscription via unsatisfiable core analysis
• Complexity-sensitive decision procedures for abstract argumentation
• Revisiting grounded circumscription in description logics
• Computing MUS-based inconsistency measures
• Synchronous counting and computational algorithm design

This page was built for publication: Counterexample guided abstraction refinement algorithm for propositional circumscription

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4930765)