A sequent calculus for circumscription | SpringerLink
Skip to main content
Springer Nature Link
Log in

A sequent calculus for circumscription

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1414))

Included in the following conference series:

Abstract

In this paper, we introduce a sequent calculus CIRC for propositional Circumscription. This work is part of a larger project, aiming at a uniform proof-theoretic reconstruction of the major families of non-monotonic logics. Among the novelties of the calculus, we mention that CIRC is analytic and comprises an axiomatic rejection method, which allows for a fully detailed formalization of the nonmonotonic aspects of inference.

We mention the semantics of negation in logic programming, inheritance in object oriented languages, and the structured operational semantics of process algebras (transition system specifications with negative premisses).

Recall that one of the original motivations of Reiter's Default Logic is modelling default values in databases.

From Levesque's system, Jiang [17] derived a resolution principle for clausal autoepistemic theories.

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.

    Article  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Article  Google Scholar 

  6. 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 

  7. P.A. Bonatti, N. Olivetti. A sequent calculus for skeptical default logic. In Proc. of TABLEAUX'97, LNAI 1227, pp. 107–121, 1997.

    Google Scholar 

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

    Article  Google Scholar 

  9. M. Cadoli, T. Eiter, G. Gottlob. An efficient method for eliminating varying predicates from a circumscription. Art. Int., 54:397–410, 1992.

    Article  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).

    Article  Google Scholar 

  12. U. Egly, H. Tompits. Non-elementary speed-ups in default reasoning. In Proceedings ECSQARU-FAPR'97, LNAI 1244, pp. 237–251, 1997.

    Google Scholar 

  13. T. Eiter, G. Gottlob. Propositional Circumscription and Extended Closed World Reasoning are π 2 inp -complete. TCS, 114:231–245, 1993.

    Article  Google Scholar 

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

    Google Scholar 

  15. 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 

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

    Article  Google Scholar 

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

    Google Scholar 

  18. P.G. Kolaitis, C.H. Papadimitriou. Some Computational Aspects of Circumscription. JACM, 37:1–14, 1990.

    Article  Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

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

    Article  Google Scholar 

  22. P. Kuhna. Circumscription and minimal models for propositional logics. In Proc. of the First Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseille, 1993.

    Google Scholar 

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

    Article  Google Scholar 

  24. V. Lifschitz. Computing Circumscription. Proc. of IJCAI'85, 121–127, 1985.

    Google Scholar 

  25. J. Lukasiewicz. Aristotle's syllogistic from the standpoint of modern formal logic. Clarendon Press, Oxford, 1951.

    Google Scholar 

  26. W. Lukaszewicz. Non-Monotonic Reasoning. Ellis Horwood Limited, Chichester, England, 1990.

    Google Scholar 

  27. J. McCarthy. Applications of circumscription in formalizing common sense knowledge. Artificial Intelligence, 28:89–116, 1986.

    Article  Google Scholar 

  28. 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 

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

    Google Scholar 

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

    Google Scholar 

  31. W. Marek, M. Truszczyński. Computing intersections of autoepistemic expansions. In [33].

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  34. I. Niemelä. Decision procedures for autoepistemic logic. Proc. LADE-88, LNCS 310, Springer-Verlag, 1988.

    Google Scholar 

  35. I. Niemelä. {cA tableau calculus for minimal model reasoning}. In Proc, of TABLEA UX'96, LNAI 1071, pp. 278–294, Springer-Verlag, Berlin, 1996.

    Google Scholar 

  36. I. Niemelä. Implementing circumscription using a tableau method. In Proc. of ECAI, John Wiley & Sons, Ltd., 1996.

    Google Scholar 

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

    Article  Google Scholar 

  38. 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 

  39. T. Przymusinski. An algorithm to compute circumscription. Art. Int., 38:49–73, 1989.

    Article  Google Scholar 

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  42. J. Schlipf. Decidability and Defmability with Circumscription. Annals of Pure and Applied Logics, 35:173–191, 1987.

    Article  Google Scholar 

  43. 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 

  44. J. Slupecki, G. Bryll, U. Wybraniec-Skardowska. Theory of rejected propositions. Studia Logica, 29:75–115, (1971).

    Article  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  47. L.Y. Yuan, C.H. Wang. On reducing parallel circumscription. Proc. of AAAI'88, 460–464, 1988.

    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

Mogens Nielsen Wolfgang Thomas

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bonatti, P.A., Olivetti, N. (1998). A sequent calculus for circumscription. In: Nielsen, M., Thomas, W. (eds) Computer Science Logic. CSL 1997. Lecture Notes in Computer Science, vol 1414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028009

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64570-2

  • Online ISBN: 978-3-540-69353-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation