Skip to main content
SpringerLink
Log in

Proof complexity of propositional default logic

  • Published:
Archive for Mathematical Logic Aims and scope Submit manuscript

Abstract

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen’s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti’s enhanced calculus for skeptical default reasoning.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Amati G., Aiello L.C., Gabbay D.M., Pirri F.: A proof theoretical approach to default reasoning I: tableaux for default logic. J. Log. Comput. 6(2), 205–231 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  2. Antoniou G.: A tutorial on default logics. ACM Comput. Surv. 31(4), 337–359 (1999)

    Article  Google Scholar 

  3. Beyersdorff, O., Meier, A., Müller, S., Thomas, M., Vollmer, H.: Proof complexity of propositional default logic. In: Proceedings of 13th International Conference on Theory and Applications of Satisfiability Testing, vol. 6175 of Lecture Notes in Computer Science, pp. 30–43. Springer, Berlin, Heidelberg (2010)

  4. Bonatti, P.A.: A Gentzen system for non-theorems. Technical Report CD/TR 93/52, Christian Doppler Labor für Expertensysteme (1993)

  5. Bonatti P.A., Olivetti N.: Sequent calculi for propositional nonmonotonic logics. ACM Trans. Comput. Log. 3(2), 226–278 (2002)

    Article  MathSciNet  Google Scholar 

  6. Bonet M.L., Buss S.R., Pitassi T.: Are there hard examples for Frege systems?. In: Clote, P., Remmel, J. (eds) Feasible Mathematics II, pp. 30–56. Birkhäuser, Basel (Boston/Stuttgart) (1995)

    Google Scholar 

  7. Bonet M.L., Pitassi T., Raz R.: On interpolation and automatization for Frege systems. SIAM J. Comput. 29(6), 1939–1967 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  8. Cadoli M., Schaerf M.: A survey of complexity results for nonmonotonic logics. J. Log. Program. 17(2/3&4), 127–160 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  9. Cook S.A., Reckhow R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  10. Dix, J., Furbach, U., Niemelä, I.: Nonmonotonic reasoning: towards efficient calculi and implementations. In: Handbook of Automated Reasoning, pp. 1241–1354. Elsevier and MIT Press (2001)

  11. Egly U., Tompits H.: Proof-complexity results for nonmonotonic reasoning. ACM Trans. Comput. Log. 2(3), 340–387 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  12. Gabbay, D.: Theoretical foundations of non-monotonic reasoning in expert systems. In: Logics and Models of Concurrent Systems, pp. 439–457. Springer, Berlin, Heidelberg (1985)

  13. Gentzen G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 68–131 (1935)

    Google Scholar 

  14. Gottlob G.: Complexity results for nonmonotonic logics. J. Log. Comput. 2(3), 397–425 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  15. Hrubeš P.: On lengths of proofs in non-classical logics. Ann. Pure Appl. Log. 157(2–3), 194–205 (2009)

    Article  MATH  Google Scholar 

  16. Jeřábek E.: Frege systems for extensible modal logics. Ann. Pure Appl. Log. 142, 366–379 (2006)

    Article  MATH  Google Scholar 

  17. Jeřábek E.: Substitution Frege and extended Frege proof systems in non-classical logics. Ann. Pure Appl. Log. 159(1–2), 1–48 (2009)

    Article  MATH  Google Scholar 

  18. Krajíček J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory, vol. 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge (1995)

    Book  Google Scholar 

  19. Kraus S., Lehmann D.J., Magidor M.: Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. 44(1–2), 167–207 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  20. Makinson, D.: General theory of cumulative inference. In: Proceedings of 2nd International Workshop on Non-Monotonic Reasoning, pp. 1–18. Springer, Berlin, Heidelberg (1989)

  21. Marek V.W., Truszczyński M.: Nonmonotonic Logics—Context-Dependent Reasoning. Springer, Berlin, Heidelberg (1993)

    Google Scholar 

  22. Reiter R.: A logic for default reasoning. Artif. Intell. 13, 81–132 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  23. Risch V., Schwind C.: Tableaux-based characterization and theorem proving for default logic. J. Autom. Reason. 13(2), 223–242 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  24. Tiomkin, M.L.: Proving unprovability. In: Proceedings of 3rd Annual Symposium on Logic in Computer Science, pp. 22–26 (1988)

Download references

Author information

Authors and Affiliations

  1. Institute of Theoretical Computer Science, Leibniz University Hanover, Hanover, Germany

    Olaf Beyersdorff, Arne Meier, Michael Thomas & Heribert Vollmer

  2. Faculty of Mathematics and Physics, Charles University Prague, Prague, Czech Republic

    Sebastian Müller

Authors
  1. Olaf Beyersdorff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arne Meier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sebastian Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Michael Thomas
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Heribert Vollmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Olaf Beyersdorff.

Additional information

An extended abstract of this article appeared in the proceedings of the conference SAT’10 [3]. Research was supported by DFG grants KO 1053/5-2 and VO 630/6-2, by a grant from the John Templeton Foundation, and by the Marie Curie FP7 Initial Training Network MALOA (no. 238381).

Rights and permissions

Reprints and permissions

About this article

Cite this article

Beyersdorff, O., Meier, A., Müller, S. et al. Proof complexity of propositional default logic. Arch. Math. Logic 50, 727–742 (2011). https://doi.org/10.1007/s00153-011-0245-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00153-011-0245-8

Keywords

Mathematics Subject Classification (2000)

Search

Navigation