Proof-complexity results for nonmonotonic reasoning

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.

REFERENCES

• 1: 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.
• 2: ANDREWS, P. B. 1971. Resolution in Type Theory. J. Symbolic Logic 36, 414-432.
• 3: Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM (JACM), v.28 n.2, p.193-214, April 1981 [doi>10.1145/322248.322249]
• 4: Krzysztof R. Apt , Howard A. Blair, Arithmetic classification of perfect models of stratified programs, Fundamenta Informaticae, v.14 n.3, p.339-343, Mar. 1991
• 5: BAAZ,M.AND LEITSCH, A. 1992. Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic 57, 181-215.
• 6: BAAZ,M.AND LEITSCH, A. 1994. On Skolemization and Proof Complexity. Fundamenta Informaticae 20, 353-379.
• 7: 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.
• 8: Rachel Ben-Eliyahu , Rina Dechter, Default reasoning using classical logic, Artificial Intelligence, v.84 n.1-2, p.113-150, July 1996 [doi>10.1016/0004-3702(95)00095-X]
• 9: BIBEL, W. 1993. Deduction: Automated Logic. Academic Press, London.
• 10: 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.
• 11: 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.
• 12: Piero A. Bonatti, Sequent Calculi for Default and Autoepistemic Logics, Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, p.127-142, May 15-17, 1996
• 13: Piero A. Bonatti , Nicola Olivetti, A Sequent Calculus for Circumscription, Selected Papers from the11th International Workshop on Computer Science Logic, p.98-114, August 23-29, 1997
• 14: Piero A. Bonatti , Nicola Olivetti, A Sequent Calculus for Skeptical Default Logic, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, p.107-121, May 13-16, 1997
• 15: Marco Cadoli, Tractable Reasoning in Artificial Intelligence, Springer-Verlag New York, Inc., Secaucus, NJ, 1995
• 16: Marco Cadoli , Francesco M. Donini, A survey on knowledge compilation, AI Communications, v.10 n.3-4, p.137-150, Dec. 1997
• 17: Marco Cadoli , Francesco M. Donini , Marco Schaerf, Is intractability of nonmonotonic reasoning a real drawback?, Artificial Intelligence, v.88 n.1-2, p.215-251, Dec. 1996 [doi>10.1016/S0004-3702(96)00009-4]
• 18: Marco Cadoli , Francesco M. Donini , Marco Schaerf , Riccardo Silvestri, On compact representations of propositional circumscription, Theoretical Computer Science, v.182 n.1-2, p.183-202, Aug. 1997 [doi>10.1016/S0304-3975(96)00182-X]
• 19: CADOLI,M.AND SCHAERF, M. 1993. A Survey of Complexity Results for Non-Monotonic Logics. J. Logic Programming 17, 127-160.
• 20: CLARK, K. L. 1978. Negation as Failure. In Logic and Databases. Plenum Press, New York, 293- 322.
• 21: Jürgen Dix , Ulrich Furbach , Ilkka Niemelä, Nonmonotonic reasoning: towards efficient calculi and implementations, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 22: DUTKIEWICZ, R. 1989. The Method of Axiomatic Rejection for the Intuitionistic Propositional Logic. Studia Logica 48, 4, 449-460.
• 23: EGLY, U. 1994. On Methods of Function Introduction and Related Concepts. Ph.D. thesis, TH Darmstadt, Alexanderstr. 10, D-64283 Darmstadt.
• 24: Uwe Egly, On different structure-preserving translations to normal form, Journal of Symbolic Computation, v.22 n.2, p.121-142, August 1996 [doi>10.1006/jsco.1996.0044]
• 25: Uwe Egly , Hans Tompits, Is Non-Monotonic Reasoning Always Harder?, Proceedings of the 4th International Conference on Logic Programming and Nonmonotonic Reasoning, p.60-75, July 28-31, 1997
• 26: Uwe Egly , Hans Tompits, Non-elementary Speed-Ups in Default Reasoning, Proceedings of the First International Joint Conference on Qualitative and Quantitative Practical Reasoning, p.237-251, June 09-12, 1997
• 27: Uwe Egly , Hans Tompits, On Proof Complexity of Circumscription, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, p.141-155, May 05-08, 1998
• 28: Thomas Eiter , Georg Gottlob, Propositional circumscription and extended closed-world reasoning are &Pgr;p2-complete, Theoretical Computer Science, v.114 n.2, p.231-245, June 21, 1993 [doi>10.1016/0304-3975(93)90073-3]
• 29: D. Gabbay, Theoretical foundations for non-monotonic reasoning in expert systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 30: GENTZEN, G. 1935. Untersuchungen uber das logische Schlieben. Mathematische Zeitschrift 39, 176-210, 405-431.
• 31: 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.
• 32: GORANKO, V. 1994. Refutation Systems in Modal Logic. Studia Logica 53, 2, 299-324.
• 33: GOTTLOB, G. 1992. Complexity Results for Nonmonotonic Logics. J. Logic and Computation 2, 397-425.
• 34: Henry A. Kautz , Bart Selman, Hard problems for simple default logics, Artificial Intelligence, v.49 n.1-3, p.243-279, May 1991 [doi>10.1016/0004-3702(91)90011-8]
• 35: 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.
• 36: Sarit Kraus , Daniel Lehmann , Menachem Magidor, Nonmonotonic reasoning, preferential models and cumulative logics, Artificial Intelligence, v.44 n.1-2, p.167-207, July 1990 [doi>10.1016/0004-3702(90)90101-5]
• 37: KREISEL,G.AND PUTNAM, H. 1957. Eine Unableitbarkeitsbeweismethode fur den Intuitionistischen Aussagenkalk ul. Archiv f ur Mathematische Logik und Grundlagenforschung 3, 74-78.
• 38: Daniel Lehmann , Menachem Magidor, What does a conditional knowledge base entail?, Artificial Intelligence, v.55 n.1, p.1-60, May 1992 [doi>10.1016/0004-3702(92)90041-U]
• 39: Alexander Leitsch, The resolution calculus, Springer-Verlag New York, Inc., New York, NY, 1997
• 40: Hector J. Levesque, All I know: a study in autoepistemic logic, Artificial Intelligence, v.42 n.2-3, p.263-309, March 1990 [doi>10.1016/0004-3702(90)90056-6]
• 41: LIFSCHITZ, V. 1985. Computing Circumscription. In Proc. 9th International Joint Conf. on Artificial Intelligence (IJCAI'85). Morgan Kaufmann, Los Altos, CA., 121-127.
• 42: Donald W Loveland, Automated theorem proving: A logical basis (Fundamental studies in computer science), sole distributor for the U.S.A. and Canada, Elsevier North-Holland, 1978
• 43: LUKASIEWICZ, J. 1951. Aristotle's Syllogistic from the Standpoint of Modern Formal Logic. Clarendon Press, Oxford.
• 44: LUKASZEWICZ, W. 1990. Non-Monotonic Reasoning: Formalization of Commonsense Reasoning. Ellis Horwood, New York.
• 45: D. Makinson, General theory of cumulative inference, Proceedings of the 2nd international workshop on Non-monotonic reasoning, p.1-18, May 1989, Grassau, Germany
• 46: MAREK, W., NERODE, A., AND REMMEL, J. 1992. A Theory of Nonmonotonic Rule Systems II. Annals of Mathematics and Artificial Intelligence 5, 229-264.
• 47: Wiktor W. Marek , M. Trusczynski , D. W. Loveland, Nonmonotonic Logic: Context-Dependent Reasoning, Springer-Verlag New York, Inc., Secaucus, NJ, 1997
• 48: MCCARTHY, J. 1980. Circumscription-A Form of Non-Monotonic Reasoning. Artificial Intelligence 13, 27-39.
• 49: M. A. Nait Abdallah, An Extended Framework for Default Reasoning, Proceedings of the International Conference on Fundamentals of Computation Theory, p.339-348, August 21-25, 1989
• 50: Ilkka N. F. Niemelä, On the decidability and complexity of autoepistemic reasoning, Fundamenta Informaticae, v.17 n.1-2, p.117-155, Sept.– Oct. 1992
• 51: 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.
• 52: Ilkka Niemelä, A Tableau Calculus for Minimal Model Reasoning, Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, p.278-294, May 15-17, 1996
• 53: OLIVETTI, N. 1992. Tableaux and Sequent Calculus for Minimal Entailment. J. of Automated Reasoning 9, 99-139.
• 54: 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.
• 55: 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.
• 56: Arkady Rabinov, A generalization of collapsible cases of circumscription, Artificial Intelligence, v.38 n.1, p.111-117, Feb. 1989 [doi>10.1016/0004-3702(89)90070-2]
• 57: REITER, R. 1978. On Closed-World Data Bases. In Logic and Databases. Plenum Press, New York, 55-76.
• 58: REITER, R. 1980. A Logic for Default Reasoning. Artificial Intelligence 13, 81-132.
• 59: RISCH,V.AND SCHWIND, C. 1994. Tableau-based Characterization and Theorem Proving for Default Logic. J. of Automated Reasoning 13, 223-242.
• 60: SCHLIPF, J. 1987. Decidability and Definability with Circumscription. Annals of Pure and Applied Logic 35, 173-191.
• 61: SCHWARZ,G.AND TRUSZCZY' NSKI, M. 1996. Nonmonotonic Reasoning is Sometimes Simpler! Journal of Logic and Computation 6, 2, 295-308.
• 62: 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.
• 63: STATMAN, R. 1979. Lower Bounds on Herbrand's Theorem. In Proc. AMS 75. 104-107.
• 64: 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.
• 65: TOMPITS, H. 1998. On Proof Complexities of First-Order Nonmonotonic Logics. Ph.D. thesis, Technische Universitat Wien, Favoritenstrasse 9-11, A-1040 Wien.
• 66: VARZI, A. 1990. Complementary Sentential Logics. Bulletin of the Section of Logic 19, 112-116.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Nonmonotonic reasoning and belief revision

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic; Proof theory; Mechanical theorem proving

General Terms:
Theory

Keywords:
circumscription, default logic, sequent calculi