ECCC-Report TR14-014https://eccc.weizmann.ac.il/report/2014/014Comments and Revisions published for TR14-014en-usFri, 31 Jan 2014 10:41:36 +0200
Paper TR14-014
| The Complexity of Theorem Proving in Circumscription and Minimal Entailment |
Olaf Beyersdorff,
Leroy Chew
https://eccc.weizmann.ac.il/report/2014/014Circumscription is one of the main formalisms for non-monotonic reasoning. It uses reasoning with minimal models, the key idea being that minimal models have as few exceptions as possible. In this contribution we provide the first comprehensive proof-complexity analysis of different proof systems for propositional circumscription. In particular, we investigate two sequent-style calculi: MLK defined by Olivetti (J. Autom. Reasoning, 1992) and CIRC introduced by Bonatti and Olivetti (ACM ToCL, 2002), and the tableaux calculus NTAB suggested by NiemelĂ¤ (TABLEAUX, 1996).
In our analysis we obtain exponential lower bounds for the proof size in NTAB and CIRC and show a polynomial simulation of CIRC by MLK. This yields a chain NTAB < CIRC < MLK of proof systems for circumscription of strictly increasing strength with respect to lengths of proofs.Fri, 31 Jan 2014 10:41:36 +0200https://eccc.weizmann.ac.il/report/2014/014