A sequent calculus for skeptical Default Logic | SpringerLink
Skip to main content
Springer Nature Link
Log in

A sequent calculus for skeptical Default Logic

  • Contributed Papers
  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1997)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1227))

Abstract

In this paper, we contribute to the proof-theory of Reiter's Default Logic by introducing a sequent calculus for skeptical reasoning. The main features of this calculus are simplicity and regularity, and the fact that proofs can be surprisingly concise and, in many cases, involve only a small part of the default theory.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Amati, L. Carlucci Aiello, D. Gabbay, F. Pirri. A proof theoretical approach to default reasoning I: tableaux for default logic. Journal of Logic and Computation, 6(2):205–231, 1996.

    Google Scholar 

  2. F. Baader, B. Hollunder. Embedding defaults into terminological knowledge representation formalisms. Journal of Automated Reasoning, 14(1):149–180, 1995.

    Google Scholar 

  3. C. Bell, A. Nerode, R. Ng and V.S. Subrahmanian. Implementing deductive databases by linear programming. In Proc. of ACM-PODS, 1992.

    Google Scholar 

  4. C. Bell, A. Nerode, R. Ng and V.S. Subrahmanian. Implementing stable semantics by linear programming. In [33].

    Google Scholar 

  5. A. Bochman. On the relation between default and modal consequence relations. In Proc of KR'94, 63–74, Morgan Kaufmann, 1994.

    Google Scholar 

  6. P.A.Bonatti. Sequent calculi for default and autoepistemic logics. In Proc. of TABLEAUX'96, LNAI 1071, pp. 127–142, Springer-Verlag, Berlin, 1996.

    Google Scholar 

  7. P.A.Bonatti. Autoepistemic logic programming. Journal of Automated Reasoning, 13:35–67, 1994.

    Google Scholar 

  8. 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, September 1993.

    Google Scholar 

  9. G. Brewka. Cumulative default logic: in defense of nonmonotonic inference rules. Artificial Intelligence 50:183–205, 1991.

    Google Scholar 

  10. X. Caicedo. A formal system for the non-theorems of the propositional calculus. Notre Dame Journal of Formal Logic, 19:147–151, (1978).

    Google Scholar 

  11. R. Dutkiewicz. The method of axiomatic rejection for the intuitionistic propositional calculus. Studia Logica, 48:449–459, (1989).

    Google Scholar 

  12. U. Egly, H. Tompits. Non-elementary speed-ups in default logic. Submitted.

    Google Scholar 

  13. D. Gabbay et al. (eds). Handbook of Logic in Artificial Intelligence and Logic Programming, Vol.III, Clarendon Press, Oxford, 1994.

    Google Scholar 

  14. D. Gabbay. Theoretical foundations for non-monotonic reasoning in expert systems. In K.R. Apt (ed.) Logics and Models of Concurrent Systems. Springer-Verlag, Berlin, 1985.

    Google Scholar 

  15. M.L. Ginsberg. A circumscriptive theorem prover. Artificial Intelligence, 39(2):209–230, (1989).

    Google Scholar 

  16. Y.J. Jiang. A first step towards autoepistemic logic programming. Computers and Artificial Intelligence, 10(5):419–441, (1992).

    Google Scholar 

  17. K. Konolige. On the Relationship between Default and Autoepistemic Logic. Artificial Intelligence, 35:343–382, 1988. + Errata, same journal, 41:115, 1989/90.

    Google Scholar 

  18. K. Konolige. On the Relation Between Autoepistemic Logic and Circumscription. In Proceedings IJCAI-89, 1989.

    Google Scholar 

  19. S. Kraus, D. Lehmann and M. Magidor. Nonmonotonic reasoning, preferential models and cumulative logics. Artificial Intelligence, 44(1):167–207, (1990).

    Google Scholar 

  20. H.J. Levesque. All I know: a study in autoepistemic logic. Artificial Intelligence, 42:263–309, (1990).

    Google Scholar 

  21. J. Łukasiewicz. Aristotle's syllogistic from the standpoint of modern formal logic. Clarendon Press, Oxford, 1951.

    Google Scholar 

  22. W. Lukasziewicz. Non-Monotonic Reasoning. Ellis Horwood Limited, Chichester, England, 1990.

    Google Scholar 

  23. J. McCarthy. Circumscription: a form of non-monotonic reasoning. Artificial Intelligence, 13:27–39, (1980).

    Google Scholar 

  24. D. Makinson. General theory of cumulative inference. In M. Reinfrank, J. De Kleer, M.L. Ginsberg and E. Sandewall (eds.) Non-monotonic Reasoning, LNAI 346, Springer-Verlag, Berlin, 1989, 1–18.

    Google Scholar 

  25. W. Marek, A. Nerode, M. Trusczyński (eds). Logic Programming and Non-monotonic Reasoning: Proc. of the Third Int. Conference. LNAI 928, Springer-Verlag, Berlin, 1995.

    Google Scholar 

  26. W. Marek, M. Truszczyński. Nonmonotonic Logics — Context-Dependent Reasoning. Springer, 1993.

    Google Scholar 

  27. W. Marek, M. Trusczyński. Computing intersections of autoepistemic expansions. In [29].

    Google Scholar 

  28. M.A. Nait Abdallah. An extended framework for default reasoning. In Proc. of FCT'89, LNCS 380, 339–348, Springer-Verlag, 1989.

    Google Scholar 

  29. A. Nerode, W. Marek, V.S. Subrahmanian (eds.). Logic Programming and Non-monotonic Reasoning: Proc. of the First Int. Workshop, MIT Press, Cambridge, Massachusetts, 1991.

    Google Scholar 

  30. I. Niemela. Decision procedures for autoepistemic logic. Proc. CADE-88, LNCS 310, Springer-Verlag, 1988.

    Google Scholar 

  31. I. Niemela. Toward efficient default reasoning. Proc. IJCAI'95, 312–318, Morgan Kaufmann, 1995.

    Google Scholar 

  32. N. Olivetti. Tableaux and sequent calculus for minimal entailment. Journal of Automated Reasoning, 9:99–139, (1992).

    Google Scholar 

  33. L. M. Pereira, A. Nerode (eds.). Logic Programming and Non-monotonic Reasoning: Proc. of the Second Int. Workshop, MIT Press, Cambridge, Massachusetts, 1993.

    Google Scholar 

  34. R. Reiter. A logic for default reasoning. Artificial Intelligence, 13:81–132, (1980).

    Google Scholar 

  35. V. Risch, C.B. Schwind. Tableau-based characterization and theorem proving for default logic. Journal of Automated Reasoning, 13:223–242, 1994.

    Google Scholar 

  36. T. Schaub. A new methodology for query answering in default logics via structureoriented theorem proving. Journal of Automated Reasoning, 15(1):95–165, 1995.

    Google Scholar 

  37. D. Scott. Completeness proofs for the intuitionistic sentential calculus. Summaries of Talks Presented at the Summer Institute for Symbolic Logic (Itaha, Cornell University, July 1957), Princeton: Institute for Defense Analyses, Communications Research Division, 1957, 231–242.

    Google Scholar 

  38. J. Słupecki, G. Bryll, U. Wybraniec-Skardowska. Theory of rejected propositions. Studia Logica, 29:75–115, (1971).

    Google Scholar 

  39. M. Tiomkin. Proving unprovability. In Proc. of LICS'88, 1988.

    Google Scholar 

  40. A. Varzi. Complementary sentential logics. Bulletin of the Section of Logic, 19:112–116, (1990).

    Google Scholar 

  41. A. Varzi. Complementary logics for classical prepositional languages. Kriterion. Zeitschrift für Philosophie, 4:20–24 (1992).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dip. di Informatica, Università di Torino, Corso Svizzera 185, I-10149, Torino, Italy

    P. A. Bonatti & N. Olivetti

Authors
  1. P. A. Bonatti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. N. Olivetti
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Didier Galmiche

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bonatti, P.A., Olivetti, N. (1997). A sequent calculus for skeptical Default Logic. In: Galmiche, D. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1997. Lecture Notes in Computer Science, vol 1227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027408

Download citation

  • DOI: https://doi.org/10.1007/BFb0027408

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62920-7

  • Online ISBN: 978-3-540-69046-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation