Non-elementary speed-ups in default reasoning

  • Uwe Egly
  • Hans Tompits
Accepted Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1244)


Default logic is one of the most prominent formalizations of common-sense reasoning. It allows “jumping to conclusions” in case that not all relevant information is known. However, theoretical complexity results imply that default logic is (in the worst case) computationally harder than classical logic. This somehow contradicts our intuition about common-sense reasoning: default rules should help to speed up the reasoning process, and not to slow it down. In this paper, we show that default logic can indeed deliver the goods. We consider a sequent-calculus for first-order default logic and show that the presence of defaults can tremendously simplify the search of proofs. In particular, we show that certain sequents have only long “classical” proofs, but short proofs can be obtained by using defaults.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Baaz and A. Leitsch. On Skolemization and Proof Complexity. Fundamenta Informaticae, 20:353–379, 1994.Google 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. In Proceedings TABLEAUX'96, Springer LNCS 1071, pp. 127–142, 1996.Google Scholar
  4. 4.
    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, pp. 946–951. MIT Press, 1994.Google Scholar
  5. 5.
    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
  6. 6.
    M. Cadoli and M. Schaerf. A Survey of Complexity Results for Non-Monotonic Logics. Journal of Logic Programming, 17:127–160, 1993.Google Scholar
  7. 7.
    U. Egly. On Methods of Function Introduction and Related Concepts. PhD thesis, Technische Hochschule Darmstadt, Alexanderstr. 10, D-64283 Darmstadt, 1994.Google Scholar
  8. 8.
    U. Egly and H. Tompits. Is Nonmonotonic Reasoning Always Harder? In Ilkka Niemelä, editor, Proceedings of the ECAI'96 Workshop on Integrating Nonmonotonicity into Automated Reasoning Systems, Fachberichte Informatik 18-96, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 1996. Scholar
  9. 9.
    T. Eiter and G. Gottlob. Propositional Circumscription and Extended Closed World Reasoning are Π 2P-complete. Journal of Theoretical Computer Science, 114(2):231–245, 1993. Addendum in vol. 118, p. 315, 1993.Google Scholar
  10. 10.
    G. Gottlob. Complexity Results for Nonmonotonic Logics. Journal of Logic and Computation, 2:397–425, 1992.Google Scholar
  11. 11.
    W. Marek, A. Nerode and J. Remmel. A Theory of Nonmonotonic Rule Systems II. Annals of Mathematics and Artificial Intelligence, 5:229–264, 1992.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
    R. Reiter. A Logic for Default Reasoning. Artificial Intelligence Journal 13, p. 81, 1980.Google Scholar
  14. 14.
    R. Reiter. Nonmonotonic Reasoning: Compiled vs. Interpreted Theories. Considerations for the Panel at Nonmon96. Proceedings of the Sixth International Workshop on Nonmonotonic Reasoning, Timberline, Oregon, 1996.Google Scholar
  15. 15.
    J. Schlipf. Decidability and Definability with Circumscription. Annals of Pure and Applied Logic, 35:173–191, 1987.Google Scholar
  16. 16.
    G. Schwarz and M. Truszczyński. Nonmonotonic Reasoning is Sometimes Simpler. Journal of Logic and Computation, 6(2):295–308, 1996.Google Scholar
  17. 17.
    A. Varzi. Complementary Sentential Logics. Bulletin of the Section of Logic, 19:112–116, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

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

Personalised recommendations