Proof complexity of propositional default logic
type: Item
instance of: scholarly article
title: Proof complexity of propositional default logic
zbMATH Open document ID: 1308.03057
author: Juan-Miguel Gracia
published in: Archive for Mathematical Logic
publication date: 2011-11-23T00:00:00Z
full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2010/2526/
review text: 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.
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B60
zbMATH DE Number: 5977561
zbMATH Keywords: default logic
zbMATH Keywords: sequent calculus
zbMATH Keywords: proof complexity
MaRDI profile type: Publication
OpenAlex ID: W1965803162
Wikidata QID: Q57998311
cites work: A proof theoretical approach to default reasoning I: tableaux for default logic
cites work: Proof Complexity of Propositional Default Logic
cites work: Q5392678
cites work: Q4850545
cites work: On Interpolation and Automatization for Frege Systems
cites work: A survey of complexity results for non-monotonic logics
cites work: The relative efficiency of propositional proof systems
cites work: Nonmonotonic reasoning: Towards efficient calculi and implementations
cites work: Proof-complexity results for nonmonotonic reasoning
cites work: Q3703316
cites work: Complexity Results for Nonmonotonic Logics
cites work: On lengths of proofs in non-classical logics
cites work: Frege systems for extensible modal logics
cites work: Substitution Frege and extended Frege proof systems in non-classical logics
cites work: Q4856172
cites work: Nonmonotonic reasoning, preferential models and cumulative logics
cites work: Q3829532
cites work: Q4273952
cites work: A logic for default reasoning
cites work: Tableau-based characterization and theorem proving for default logic
DOI: 10.1007/S00153-011-0245-8
Recommended article: Proof Complexity of Propositional Default Logic
Recommended article: The Complexity of Reasoning for Fragments of Default Logic
Recommended article: Q5193024
Recommended article: Symbolic and Quantitative Approaches to Reasoning with Uncertainty
Recommended article: Sequent calculi for default and autoepistemic logics
Recommended article: On the computational complexity of assumption-based argumentation for default reasoning.
Recommended article: A sequent calculus for skeptical Default Logic
Recommended article: The Complexity of Theorem Proving in Autoepistemic Logic
Recommended article: Hard problems for simple default logics
Recommended article: Q3493327
description: scientific article; zbMATH DE number 5977561