The Complexity of Theorem Proving in Circumscription and Minimal Entailment

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 [28] and CIRC introduced by Bonatti and Olivetti [8], and the tableaux calculus NTAB suggested by Niemela [26]. 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 <(p) CIRC <(p) MLK of proof systems for circumscription of strictly increasing strength with respect to lengths of proofs.