Proof complexity of propositional default logic
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.
- Proof complexity of propositional default logic
- The Complexity of Reasoning for Fragments of Default Logic
- Axiomatization of credulous reasoning in rational default logic
- A sequent calculus for skeptical reasoning in predicate default logic (extended abstract)
- Sequent calculi for default and autoepistemic logics
- On the computational complexity of assumption-based argumentation for default reasoning.
- A sequent calculus for skeptical Default Logic
- The complexity of theorem proving in autoepistemic logic
- Hard problems for simple default logics
- scientific article; zbMATH DE number 4166939
- A logic for default reasoning
- A proof theoretical approach to default reasoning I: tableaux for default logic
- A survey of complexity results for non-monotonic logics
- Complexity Results for Nonmonotonic Logics
- Frege systems for extensible modal logics
- scientific article; zbMATH DE number 3930376 (Why is no real title available?)
- scientific article; zbMATH DE number 4104920 (Why is no real title available?)
- scientific article; zbMATH DE number 478394 (Why is no real title available?)
- scientific article; zbMATH DE number 806744 (Why is no real title available?)
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 5877692 (Why is no real title available?)
- Nonmonotonic reasoning, preferential models and cumulative logics
- Nonmonotonic reasoning: Towards efficient calculi and implementations
- On Interpolation and Automatization for Frege Systems
- On lengths of proofs in non-classical logics
- Proof complexity of propositional default logic
- Proof-complexity results for nonmonotonic reasoning
- Substitution Frege and extended Frege proof systems in non-classical logics
- Tableau-based characterization and theorem proving for default logic
- The relative efficiency of propositional proof systems
- scientific article; zbMATH DE number 1123617 (Why is no real title available?)
- Restricted default theories: expressive power and outlier detection tasks
- Proof complexity of propositional default logic
- The complexity of theorem proving in autoepistemic logic
- Proof complexity of non-classical logics
- A sequent calculus for skeptical reasoning in predicate default logic (extended abstract)
- Proof Complexity of Non-classical Logics
- Sequent-type rejection systems for finite-valued non-deterministic logics
- Strong backdoors for default logic
- Strong backdoors for default logic
- Proof complexity of modal resolution
- On the complexity of extension checking in default logic
This page was built for publication: Proof complexity of propositional default logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q647339)
