On Proof Complexity of Circumscription

  • Uwe Egly
  • Hans Tompits
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


Circumscription is a non-monotonic formalism based on the idea that objects satisfying a certain predicate expression are considered as the only objects satisfying it. Theoretical complexity results imply that circumscription is (in the worst case) computationally harder than classical logic. This somehow contradicts our intuition about common- sense reasoning: non-monotonic rules should help to speed up the reasoning process, and not to slow it down.

In this paper, we consider a first-order sequent calculus for circumscription and show that the presence of circumscription rules can tremendously simplify the search for proofs. In particular, we show that certain sequents have only long “classical” proofs, but short proofs can be obtained by using circumscription.


Predicate Symbol Propositional Atom Sequent Calculus Default Logic Nonmonotonic Reasoning 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    G. Amati, L. C. Aiello, D. Gabbay and F. Pirri. A Proof Theoretical Approach to Default Reasoning I: Tableaux for Default Logic. Journal of Logic and Computation, 6(2):205–231, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    P. A. Bonatti. A Gentzen System for Non-Theorems. Technical Report CD-TR 93/52, Christian Doppler Labor für Expertensysteme, Technische Universität Wien, Paniglgasse 16, A-1040 Wien, 1993.Google Scholar
  3. 3.
    P. A. Bonatti. Sequent Calculi for Default and Autoepistemic Logics. Proceedings TABLEAUX’96, Springer LNAI 1071, pp. 127–142, 1996.Google Scholar
  4. 4.
    P. A. Bonatti and N. Olivetti. A Sequent Calculus for Skeptical Default Logic. Proceedings TABLEAUX’97, Springer LNAI 1227, pp. 107–121, 1997.Google Scholar
  5. 5.
    P.A. Bonatti and N. Olivetti. A Sequent Calculus for Circumscription. Preliminary Proceedings CSL’97, BRICS Notes Series NS-97-1, pp. 95–107, 1997.Google Scholar
  6. 6.
    M. Cadoli, F. M. Donini, and M. Schaerf. Is Intractability of Non-Monotonic Reasoning a Real Drawback? In Proceedings of the AAAI National Conference on Artificial Intelligence, pages 946–951. MIT Press, 1994.Google Scholar
  7. 7.
    M. Cadoli, F. M. Donini, and M. Schaerf. On Compact Representation of Propositional Circumscription. In Proceedings STACS’ 95, Springer LNCS 900, pp. 205–216, 1995.Google Scholar
  8. 8.
    M. Cadoli and M. Schaerf. A Survey of Complexity Results for Non-Monotonic Logics. Journal of Logic Programming, 17:127–160, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    K. L. Clark. Negation as Failure. In Logic and Databases, Plenum, New York, pp. 293–322, 1978.Google Scholar
  10. 10.
    U. Egly and H. Tompits. Is Nonmonotonic Reasoning Always Harder? Proceedings LPNMR’97, Springer LNAI 1265, pp. 60–75, 1997.Google Scholar
  11. 11.
    U. Egly and H. Tompits. Non-Elementary Speed-Ups in Default Reasoning. Proceedings ECSQARU-FAPR’97, Springer LNAI 1244, pp. 237–251, 1997.Google Scholar
  12. 12.
    T. Eiter and G. Gottlob. Propositional Circumscription and Extended Closed World Reasoning are II 2P-complete. Journal of Theoretical Computer Science, 114(2):231–245, 1993. Addendum: vol. 118, p. 315, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    V. Goranko. Refutation Systems in Modal Logic. Studia Logica, 53(2):299–324, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    G. Gottlob. Complexity Results for Nonmonotonic Logics. Journal of Logic and Computation, 2:397–425, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    H. A. Kautz and B. Selman. Hard Problems for Simple Default Logics. Artificial Intelligence, 49:243–379, 1990.CrossRefMathSciNetGoogle Scholar
  16. 16.
    V. Lifschitz. Computing Circumscription. In Proceedings of IJCAI’85, Morgan Kaufmann, Los Altos, CA, pp. 121–127, 1985.Google Scholar
  17. 17.
    J. Łukasiewicz. Aristotle’s Syllogistic from the Standpoint of Modern Formal Logic. Clarendon Press, Oxford, 1951.zbMATHGoogle Scholar
  18. 18.
    W. Marek, A. Nerode and J. Remmel. A Theory of Nonmonotonic Rule Systems II. Annals of Mathematics and Artificial Intelligence, 5:229–264, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    J. McCarthy. Epistemological Problems of Artificial Intelligence. In Proceedings of IJCAI’77, Cambridge, MA, pp. 1038–1044, 1977.Google Scholar
  20. 20.
    J. McCarthy. Circumscription — A Form of Non-Monotonic Reasoning. Artificial Intelligence, 13:27–39, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    I. Niemelä. A Tableau Calculus for Minimal Model Reasoning. Proceedings TABLEAUX’96, Springer LNAI 1071, pp. 278–294, 1996.Google Scholar
  22. 22.
    I. Niemelä. Implementing Circumscription Using a Tableau Method. Proceedings ECAI’96, John Wiley & Sons Ltd., Chichester, pp. 80–84, 1996.Google Scholar
  23. 23.
    N. Olivetti. Tableaux and Sequent Calculus for Minimal Entailment. Journal of Automated Reasoning, 9:99–139, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    V. P. Orevkov. Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR, 88:137–161, 1979. English translation in Journal of Soviet Mathematics, 2337–2350, 1982.zbMATHMathSciNetGoogle Scholar
  25. 25.
    R. Reiter. On Closed-World Data Bases. In Logic and Databases, pp. 55–76, Plenum, New York, 1978.Google Scholar
  26. 26.
    J. Schlipf. Decidability and Definability with Circumscription. Annals of Pure and Applied Logic, 35:173–191, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    A. Varzi. Complementary Sentential Logics. Bulletin of the Section of Logic, 19:112–116, 1990.MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Uwe Egly
    • 1
  • Hans Tompits
    • 1
  1. 1.Abt. Wissensbasierte Systeme 184/3Technische Universität WienWienAustria

Personalised recommendations