Abstract
Although it has been shown that non-monotonic reasoning is presumably harder than classical reasoning, there are cases where a non-monotonic treatment actually simplifies matters. Indeed, one of the reasons for considering non-monotonic systems is the hope of speeding up reasoning, and not to slow it down. In this paper, we consider proof lengths in a cut-free sequent calculus, and we show that the application of circumscription (or completion) to certain first-order formulae leads to a non-elementary speed-up of proof length. This is possible because the introduction of the completion formula can simulate the cut rule.
The authors would like to thank Georg Gottlob and Thomas Eiter for their useful comments and constructive criticisms on an earlier version of this paper. The first author was partly supported by the Christian Doppler Labor für Expertensysteme, Wien, Austria.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Baaz and A. Leitsch. Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic, 57:181–215, 1992.
M. Baaz and A. Leitsch. On Skolemization and Proof Complexity. Fundamenta Informaticae, 20:353–379, 1994.
R. Ben-Eliyahu and R. Dechter. Default Logic, Propositional Logic and Constraints. In Proceedings of the AAAI National Conference on Artificial Intelligence, Los Altos, CA, 1991. Morgan Kaufmann.
W. Bibel. Deduction: Automated Logic. Academic Press, London, 1993.
P. A. Bonatti. Proof Systems for Default and Autoepistemic Logics. In P. Miglioli, U. Moscato, D. Mundici and M. Ornaghi, editors, Proceedings TABLEAUX'96, Springer LNCS 1071, pp. 127–142, 1996.
M. Cadoli, F. M. Donini, and M. Schaerf. Is Intractability of Non-Monotonic Reasoninga Real Drawback? In Proceedings of the AAAI National Conference on Artificial Intelligence, pages 946–951. MIT Press, 1994.
M. Cadoli, F. M. Donini, and M. Schaerf. On Compact Representation of Propositional Circumscription. In Proceedings STAGS '95, Springer LNCS 900, pp. 205–216, 1995.
M. Cadoli and M. Schaerf. A Survey of Complexity Results for Non-Monotonic Logics. Journal of Logic Programming, 17:127–160, 1993.
W. F. Dowling and J. H. Gallier. Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. Journal of Logic Programming, 3:267–284, 1984.
U. Egly. On Methods of Function Introduction and Related Concepts. PhD thesis, Technische Hochschule Darmstadt, Alexanderstr. 10, D-64283 Darmstadt, 1994.
U. Egly. On Different Structure-Preserving Translations to Normal Form, 1996. Journal of Symbolic Computation, 22:121–142.
U. Egly and H. Tompits. Non-Elementary Speed-Ups in Default Reasoning. To appear in Proceedings ECSQARU'97, Springer 1997.
T. Eiter and G. Gottlob. Propositional Circumscription and Extended Closed World Reasoning are Π P 2-complete. Journal of Theoretical Computer Science, 114(2):231–245, 1993. Addendum: vol. 118, p. 315, 1993.
G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.
G. Gottlob. Complexity Results for Nonmonotonic Logics. Journal of Logic and Computation, 2:397–425, 1992.
H. A. Kautz and B. Selman. Hard Problems for Simple Default Logics. Artificial Intelligence, 49:243–379, 1990.
V. Lifschitz. Computing Circumscription. In Proceedings of IJCAI-85, pages 121–127, Los Altos, CA., 1985. Morgan Kaufmann.
I. Niemelä. On the Decidability and Complexity of Autoepistemic Reasoning. Fundamenta Informaticae, 17:117–155, 1992.
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.
J. Schlipf. Decidability and Definability with Circumscription. Annals of Pure and Applied Logic, 35:173–191, 1987.
G. Schwarz and M. Truszczyński. Nonmonotonic Reasoning is Sometimes Simpler. Journal of Logic and Computation, 6(2):295–308, 1996.
R. Statman. Lower Bounds on Herbrand's Theorem. In Proc. AMS 75, pages 104–107, 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Egly, U., Tompits, H. (1997). Is non-monotonic reasoning always harder. In: Dix, J., Furbach, U., Nerode, A. (eds) Logic Programming And Nonmonotonic Reasoning. LPNMR 1997. Lecture Notes in Computer Science, vol 1265. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63255-7_5
Download citation
DOI: https://doi.org/10.1007/3-540-63255-7_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63255-9
Online ISBN: 978-3-540-69249-2
eBook Packages: Springer Book Archive