Skip to main content
SpringerLink
Log in

The Complexity of Theorem Proving in Circumscription and Minimal Entailment

  • Conference paper
Automated Reasoning (IJCAR 2014)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8562))

Included in the following conference series:

Abstract

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 Niemelä [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.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Beyersdorff, O.: The complexity of theorem proving in autoepistemic logic. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 365–376. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  2. Beyersdorff, O., Galesi, N., Lauria, M.: A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games. Inf. Process. Lett. 110(23), 1074–1077 (2010)

    Article  MathSciNet  Google Scholar 

  3. Beyersdorff, O., Köbler, J., Messner, J.: Nondeterministic functions and the existence of optimal proof systems. Theor. Comput. Sci. 410(38-40), 3839–3855 (2009)

    Article  MATH  Google Scholar 

  4. Beyersdorff, O., Kutz, O.: Proof complexity of non-classical logics. In: Bezhanishvili, N., Goranko, V. (eds.) ESSLLI 2010/2011, Lectures. LNCS, vol. 7388, pp. 1–54. Springer, Heidelberg (2012)

    Google Scholar 

  5. Beyersdorff, O., Meier, A., Müller, S., Thomas, M., Vollmer, H.: Proof complexity of propositional default logic. Archive for Mathematical Logic 50(7), 727–742 (2011)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  7. Bonatti, P.A., Lutz, C., Wolter, F.: The complexity of circumscription in DLs. J. Artif. Intell. Res (JAIR) 35, 717–773 (2009)

    MATH  MathSciNet  Google Scholar 

  8. Bonatti, P.A., Olivetti, N.: Sequent calculi for propositional nonmonotonic logics. ACM Transactions on Computational Logic 3(2), 226–278 (2002)

    Article  MathSciNet  Google Scholar 

  9. Bonet, M.L., Pitassi, T., Raz, R.: On interpolation and automatization for Frege systems. SIAM Journal on Computing 29(6), 1939–1967 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  10. Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. The Journal of Symbolic Logic 52, 916–927 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  11. Cadoli, M., Lenzerini, M.: The complexity of propositional closed world reasoning and circumscription. J. Comput. Syst. Sci. 48(2), 255–310 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  12. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic 44(1), 36–50 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  13. Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  14. Durand, A., Hermann, M., Nordh, G.: Trichotomies in the complexity of minimal inference. Theory Comput. Syst. 50(3), 446–491 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  15. Egly, U., Tompits, H.: Proof-complexity results for nonmonotonic reasoning. ACM Transactions on Computational Logic 2(3), 340–387 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  16. Eiter, T., Gottlob, G.: Propositional circumscription and extended closed world reasoning are \(\Pi_2^p\)-complete. Theor. Comput. Sci. 114(2), 231–245 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  17. Fenner, S.A., Fortnow, L., Naik, A.V., Rogers, J.D.: Inverting onto functions. Information and Computation 186(1), 90–103 (2003)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  19. Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  20. Hrubeš, P.: On lengths of proofs in non-classical logics. Annals of Pure and Applied Logic 157(2-3), 194–205 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  21. Janota, M., Marques-Silva, J.: cmMUS: A tool for circumscription-based MUS membership testing. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS (LNAI), vol. 6645, pp. 266–271. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. Jeřábek, E.: Substitution Frege and extended Frege proof systems in non-classical logics. Annals of Pure and Applied Logic 159(1-2), 1–48 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  23. Krajíček, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press (1995)

    Google Scholar 

  24. McCarthy, J.: Circumscription – a form of non-monotonic reasoning. Artificial Intelligence 13, 27–39 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  25. Niemelä, I.: Implementing circumscription using a tableau method. In: ECAI, pp. 80–84 (1996)

    Google Scholar 

  26. Niemelä, I.: A tableau calculus for minimal model reasoning. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 278–294. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  27. Nieuwenhuis, R.: SAT and SMT are still resolution: Questions and challenges. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 10–13. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  28. Olivetti, N.: Tableaux and sequent calculus for minimal entailment. J. Autom. Reasoning 9(1), 99–139 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  29. Thomas, M.: The complexity of circumscriptive inference in Post’s lattice. Theory of Computing Systems 50(3), 401–419 (2012)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing, University of Leeds, UK

    Olaf Beyersdorff & Leroy Chew

Authors
  1. Olaf Beyersdorff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Leroy Chew
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS,, New York University &amp, USA

    Stéphane Demri

  2. Department of Computer Science, University of New Mexico, 87131-0001, Albuquerque, NM, USA

    Deepak Kapur

  3. Max Planck Institute for Informatics, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Beyersdorff, O., Chew, L. (2014). The Complexity of Theorem Proving in Circumscription and Minimal Entailment. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08587-6_32

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08586-9

  • Online ISBN: 978-3-319-08587-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation