Uwe Egly
Skip Abstract Section
Abstract
It is well-known that almost all nonmonotonic formalisms have a higher worst-case complexity than classical reasoning. In some sense, this observation denies one of the original motivations of nonmonotonic systems, which was the expectation taht nonmonotonic rules should help to speed-up the reasoning process, and not make it more difficult. In this paper, we look at this issue from a proof-theoretical perspective. We consider analytic calculi for certain nonmonotonic logis and analyze to what extent the presence of nonmonotonic rules can simplify the search for proofs. In particular, we show that there are classes of first-order formulae which have only extremely long “classical” proofs, i.e., proofs without applications of nonmonotonic rules, but there are short proofs using nonmonotonic inferences. Hence,despite the increase of complexity in the worst case, there are instances where nonmonotonic reasoning can be much simpler than classical (cut-free) reasoning.
- AMATI, G., AIELLO,L.C.,GABBAY,D.,AND PIRRI, F. 1996. A Proof Theoretical Approach to Default Reasoning I: Tableaux for Default Logic. J. of Logic and Computation 6, 2, 205-231.Google Scholar
- ANDREWS, P. B. 1971. Resolution in Type Theory. J. Symbolic Logic 36, 414-432.Google Scholar
- ANDREWS, P. B. 1981. Theorem Proving via General Matings. J. ACM 28, 2, 193-214. Google Scholar
- APT,K.R.AND BLAIR, H. A. 1990. Arithmetic Classification of Perfect Models of Stratified Programs. Fundamenta Informaticae 13, 1-18. Addendum in 14:339-343, 1991. Google Scholar
- BAAZ,M.AND LEITSCH, A. 1992. Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic 57, 181-215.Google Scholar
- BAAZ,M.AND LEITSCH, A. 1994. On Skolemization and Proof Complexity. Fundamenta Informaticae 20, 353-379.Google Scholar
- BEN-ELIYAHU,R.AND DECHTER, R. 1991. Default Logic, Propositional Logic and Constraints. In Proc. 9th National Conf. on Artificial Intelligence (AAAI'91). Morgan Kaufmann, Los Altos, CA, 379-385.Google Scholar
- BEN-ELIYAHU,R.AND DECHTER, R. 1996. Default Reasoning using Classical Logic. Artificial Intelligence 84, 113-150. Google Scholar
- BIBEL, W. 1993. Deduction: Automated Logic. Academic Press, London.Google Scholar
- BOCHMAN, A. 1994. On the Relation Between Default and Modal Consequence Relations. In Proc. 4th International Conf. on Principles of Knowledge Representation and Reasoning (KR'94). Morgan Kaufmann, San Francisco, 63-74.Google Scholar
- BONATTI, P. A. 1993. A Gentzen System for Non-Theorems. Tech. Rep. CD-TR 93/52, Christian Doppler Labor f ur Expertensysteme, Technische Universit at Wien.Google Scholar
- BONATTI, P. A. 1996. Sequent Calculi for Default and Autoepistemic Logics. In Proc. International Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'96). Lecture Notes in Artificial Intelligence, vol. 1071. Springer Verlag, Berlin, 127-142. Google Scholar
- BONATTI,P.A.AND OLIVETTI, N. 1997a. A Sequent Calculus for Circumscription. In Proc. 11th International Workshop on Computer Science Logic (CSL'97). Lecture Notes in Computer Science, vol. 1414. Springer Verlag, Berlin, 98-114. Google Scholar
- BONATTI,P.A.AND OLIVETTI, N. 1997b. A Sequent Calculus for Skeptical Default Logic. In Proc. International Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'97). Lecture Notes in Artificial Intelligence, vol. 1227. Springer Verlag, Berlin, 107-121. Google Scholar
- CADOLI, M. 1995. Tractable Reasoning in Artificial Intelligence. Lecture Notes in Artificial Intelligence, vol. 941. Springer Verlag, Berlin. Google Scholar
- CADOLI,M.AND DONINI, F. M. 1997. A Survey on Knowledge Compilation. AI Communications 10, 137-150. Google Scholar
- CADOLI, M., DONINI,F.M.,AND SCHAERF, M. 1996. Is Intractability of Non-Monotonic Reasoning a Real Drawback? Artificial Intelligence 88, 215-251. Google Scholar
- CADOLI, M., DONINI, F. M., SCHAERF, M., AND SILVESTRI, R. 1997. On Compact Representations of Propositional Circumscription. Theoretical Computer Science 182, 183-202. Google Scholar
- CADOLI,M.AND SCHAERF, M. 1993. A Survey of Complexity Results for Non-Monotonic Logics. J. Logic Programming 17, 127-160.Google Scholar
- CLARK, K. L. 1978. Negation as Failure. In Logic and Databases. Plenum Press, New York, 293- 322.Google Scholar
- DIX, J., FURBACH,U.,AND NIEMEL A, I. 2001. Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations. In Handbook of Automated Reasoning. Elsevier Science Press, 1121-1134. Google Scholar
- DUTKIEWICZ, R. 1989. The Method of Axiomatic Rejection for the Intuitionistic Propositional Logic. Studia Logica 48, 4, 449-460.Google Scholar
- EGLY, U. 1994. On Methods of Function Introduction and Related Concepts. Ph.D. thesis, TH Darmstadt, Alexanderstr. 10, D-64283 Darmstadt.Google Scholar
- EGLY, U. 1996. On Different Structure-Preserving Translations to Normal Form. J. Symbolic Computation 22, 121-142. Google Scholar
- EGLY,U.AND TOMPITS, H. 1997a. Is Non-Monotonic Reasoning Always Harder? In Proc. 4th International Conf. on Logic Programing and Nonmonotonic Reasoning (LPNMR'97). Lecture Notes in Artificial Intelligence, vol. 1265. Springer Verlag, Berlin, 60-75. Google Scholar
- EGLY,U.AND TOMPITS, H. 1997b. Non-Elementary Speed-Ups in Default Reasoning. In Proc. 1st International Joint Conf. on Qualitative and Quantitative Practical Reasoning (ECSQARU-FAPR'97). Lecture Notes in Artificial Intelligence, vol. 1244. Springer Verlag, Berlin, 237- 251. Google Scholar
- EGLY,U.AND TOMPITS, H. 1998. On Proof Complexity of Circumscription. In Proc. International Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98). Lecture Notes in Artificial Intelligence, vol. 1397. Springer Verlag, Berlin, 141-155. Google Scholar
- EITER,T.AND GOTTLOB, G. 1993. Propositional Circumscription and Extended Closed World Reasoning are 5 P2 -complete. J. Theoretical Computer Science 144, 2, 231-245. Addendum: vol. 118, p. 315, 1993. Google Scholar
- GABBAY, D. 1985. Theoretical Foundations for Non-Monotonic Reasoning in Expert Systems. In Logics and Models of Concurrent Systems. Springer Verlag, Berlin, 439-457. Google Scholar
- GENTZEN, G. 1935. Untersuchungen uber das logische Schlieben. Mathematische Zeitschrift 39, 176-210, 405-431.Google Scholar
- GOGIC, G., PAPADIMITROU, C., SELMAN,B.,AND KAUTZ, H. 1995. The Comparative Linguistics of Knowledge Representation. In Proc. 14th International Joint Conf. on Artificial Intelligence (IJCAI'95). Morgan Kaufmann, San Mateo, 862-869. Google Scholar
- GORANKO, V. 1994. Refutation Systems in Modal Logic. Studia Logica 53, 2, 299-324.Google Scholar
- GOTTLOB, G. 1992. Complexity Results for Nonmonotonic Logics. J. Logic and Computation 2, 397-425.Google Scholar
- KAUTZ,H.A.AND SELMAN, B. 1990. Hard Problems for Simple Default Logics. Artificial Intelligence 49, 243-379. Google Scholar
- KOLAITIS,P.AND PAPADIMITRIOU, C. 1988. Some Computational Aspects of Circumscription. In Proc. 7th National Conf. on Artificial Intelligence (AAAI'88). MIT Press, Menlo Park, 465-469.Google Scholar
- KRAUS, S., LEHMANN,D.,AND MAGIDOR, M. 1990. Nonmonotonic Reasoning, Preferential Models and Cumulative Logics. Artificial Intelligence 44, 167-207. Google Scholar
- KREISEL,G.AND PUTNAM, H. 1957. Eine Unableitbarkeitsbeweismethode fur den Intuitionistischen Aussagenkalk ul. Archiv f ur Mathematische Logik und Grundlagenforschung 3, 74-78.Google Scholar
- LEHMANN,D.AND MAGIDOR, M. 1992. What does a Conditional Knowledge Base Entail? Artificial Intelligence 55, 1-60. Google Scholar
- LEITSCH, A. 1997. The Resolution Calculus. Springer Verlag, Berlin. Google Scholar
- LEVESQUE, H. J. 1990. All I Know: A Study in Autoepistemic Logic. Artificial Intelligence 42, 263-309. Google Scholar
- LIFSCHITZ, V. 1985. Computing Circumscription. In Proc. 9th International Joint Conf. on Artificial Intelligence (IJCAI'85). Morgan Kaufmann, Los Altos, CA., 121-127.Google Scholar
- LOVELAND, D. W. 1978. Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science, vol. 6. North-Holland Publishing Company, Amsterdam, New York, Oxford. Google Scholar
- LUKASIEWICZ, J. 1951. Aristotle's Syllogistic from the Standpoint of Modern Formal Logic. Clarendon Press, Oxford.Google Scholar
- LUKASZEWICZ, W. 1990. Non-Monotonic Reasoning: Formalization of Commonsense Reasoning. Ellis Horwood, New York.Google Scholar
- MAKINSON, D. 1989. General Theory of Cumulative Inference. In Proc. 2nd International Workshop on Non-Monotonic Reasoning. Lecture Notes in Artificial Intelligence, vol. 346. Springer Verlag, Berlin, 1-18. Google Scholar
- MAREK, W., NERODE, A., AND REMMEL, J. 1992. A Theory of Nonmonotonic Rule Systems II. Annals of Mathematics and Artificial Intelligence 5, 229-264.Google Scholar
- MAREK,W.AND TRUSZCZY' NSKI, M. 1993. Nonmonotonic Logic: Context-Dependent Reasoning. Springer Verlag, Berlin. Google Scholar
- MCCARTHY, J. 1980. Circumscription-A Form of Non-Monotonic Reasoning. Artificial Intelligence 13, 27-39.Google Scholar
- NAIT ABDALLAH, M. A. 1989. An Extended Framework for Default Reasoning. In Proc. International Conf. on Fundamentals of Computation Theory (FCT'89). Lecture Notes in Computer Science, vol. 380. Springer Verlag, New York, 339-348. Google Scholar
- NIEMELA, I. 1992. On the Decidability and Complexity of Autoepistemic Reasoning. Fundamenta Informaticae 17, 117-155. Google Scholar
- NIEMELA, I. 1996a. Implementing Circumscription Using a Tableau Method. In Proc. 12th European Conf. on Artificial Intelligence (ECAI'96). John Wiley & Sons, Chichester, 80-84.Google Scholar
- NIEMELA, I. 1996b. A Tableau Calculus for Minimal Model Reasoning. In Proc. International Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'96). Lecture Notes in Artificial Intelligence, vol. 1071. Springer Verlag, Berlin, 278-294. Google Scholar
- OLIVETTI, N. 1992. Tableaux and Sequent Calculus for Minimal Entailment. J. of Automated Reasoning 9, 99-139.Google Scholar
- OREVKOV, V. P. 1979. 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. English translation in J. Soviet Mathematics, 2337-2350, 1982.Google Scholar
- PINTO,L.AND DYCKHOFF, R. 1995. Loop-Free Construction of Counter-Models for Intuitionistic Propositional Logic. In Symposia Gaussiana. Walter de Gruyter & Co, Berlin, 225-232.Google Scholar
- RABINOV, A. 1989. A Generalization of Collapsible Cases of Circumscription. Artificial Intelligence 38, 111-117. Google Scholar
- REITER, R. 1978. On Closed-World Data Bases. In Logic and Databases. Plenum Press, New York, 55-76.Google Scholar
- REITER, R. 1980. A Logic for Default Reasoning. Artificial Intelligence 13, 81-132.Google Scholar
- RISCH,V.AND SCHWIND, C. 1994. Tableau-based Characterization and Theorem Proving for Default Logic. J. of Automated Reasoning 13, 223-242.Google Scholar
- SCHLIPF, J. 1987. Decidability and Definability with Circumscription. Annals of Pure and Applied Logic 35, 173-191.Google Scholar
- SCHWARZ,G.AND TRUSZCZY' NSKI, M. 1996. Nonmonotonic Reasoning is Sometimes Simpler! Journal of Logic and Computation 6, 2, 295-308.Google Scholar
- SKURA, T. 1996. Refutations and Proofs in S4. In Proof Theory of Modal Logic. Applied Logic Series, vol. 2. Kluwer Academic Publishers, Dordrecht, 45-51.Google Scholar
- STATMAN, R. 1979. Lower Bounds on Herbrand's Theorem. In Proc. AMS 75. 104-107.Google Scholar
- STILLMAN, J. 1992. The Complexity of Propositional Default Logics. In Proc. 10th National Conf. on Artificial Intelligence (AAAI'92). MIT Press, Menlo Park, 794-799.Google Scholar
- TOMPITS, H. 1998. On Proof Complexities of First-Order Nonmonotonic Logics. Ph.D. thesis, Technische Universitat Wien, Favoritenstrasse 9-11, A-1040 Wien.Google Scholar
- VARZI, A. 1990. Complementary Sentential Logics. Bulletin of the Section of Logic 19, 112-116.Google Scholar
Index Terms
- Proof-complexity results for nonmonotonic reasoning
Recommendations
Sequent calculi for propositional nonmonotonic logics
A uniform proof-theoretic reconstruction of the major nonmonotonic logics is introduced. It consists of analytic sequent calculi where the details of nonmonotonic assumption making are modelled by an axiomatic rejection method. Another distinctive ...
Sequent calculi for skeptical reasoning in predicate default logic and other nonmonotonic logics
Sequent calculi for skeptical consequence in predicate default logic, predicate stable model logic programming, and infinite autoepistemic theories are presented and proved sound and complete. While skeptical consequence is decidable in the finite ...
Proof theory of Nelson's paraconsistent logic: A uniform perspective
The aim of this paper is to obtain a theoretical foundation of inconsistency-tolerant (or paraconsistent) reasoning by presenting a comprehensive study of the structural proof-theory of David Nelson's paraconsistent logic. Inconsistency handling has a ...
Comments