Proof complexity of propositional default logic (Q647339)

The authors investigate the proof complexity of several proof systems for \textit{R. Reiter}'s propositional default logic [Artif. Intell. 13, 81--132 (1980; Zbl 0435.68069)], which is the most common formalism for nonmonotone reasoning. First, they show that the calculus of \textit{P. A. Bonatti} and \textit{N. Olivetti} [ACM Trans. Comput. Log. 3, 226--278 (2002)] for the \(\Sigma^p_2\)-complete \textit{credulous} default reasoning is essentially equivalent to the classical sequent calculus LK, in that bounds on the minimal length of LK-proofs in terms of the length of the input sequent also apply to the \(\mathrm{BO}_{\mathrm{cred}}\) calculus up to a polynomial increase, and nonautomatizability results for LK carry over to \(\mathrm{BO}_{\mathrm{cred}}\). The same also holds for the residual calculus RC embedded in \(\mathrm{BO}_{\mathrm{cred}}\). Moreover, the authors describe how to extend any given classical propositional proof system \(P\) to an equivalent proof system for credulous default reasoning. Bonatti and Olivetti [loc. cit.] also proposed calculi for the \(\Pi^p_2\)-complete \textit{skeptical} default reasoning and gave an exponential lower bound on the length of proofs in their basic calculus. This is improved in the reviewed paper to show an exponential lower bound on Bonatti and Olivetti's enhanced skeptical calculus.