Skip to main content

Interpolation Theorems for Nonmonotonic Reasoning Systems

  • Conference paper
  • First Online:
Logics in Artificial Intelligence (JELIA 2002)

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

Included in the following conference series:

Abstract

Craig’s interpolation theorem [3] is an important theorem known for propositional logic and first-order logic. It says that if a logical formula ß logically follows from a formula ∞, then there is a formula γ, including only symbols that appear in both ∞, ß, such that ß logically follows from γ and γ logically follows from ∞. Such theorems are important and useful for understanding those logics in which they hold as well as for speeding up reasoning with theories in those logics. In this paper we present interpolation theorems in this spirit for three nonmonotonic systems: circumscription, default logic and logic programs with the stable models semantics (a.k.a. answer set semantics). These results give us better understanding of those logics, especially in contrast to their nonmonotonic characteristics. They suggest that some monotonicity principle holds despite the failure of classic monotonicity for these logics. Also, they sometimes allow us to use methods for the decomposition of reasoning for these systems, possibly increasing their applicability and tractability. Finally, they allow us to build structured representations that use those logics.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Amir. (De)composition of situation calculus theories. In Proc. AAAI’ 00, pages 456–463. AAAI Press/MIT Press, 2000.

    Google Scholar 

  2. E. Amir and S. McIlraith. Paritition-based logical reasoning. In Proc. KR’ 2000, pages 389–400, 2000.

    Google Scholar 

  3. W. Craig. Linear reasoning. a new form of the Herbrand-Gentzen theorem. J. of Symbolic Logic, 22:250–268, 1957.

    MATH  MathSciNet  Google Scholar 

  4. A. Darwiche. Model-based diagnosis using structured system descriptions. Journal of AI Research, 8: 165–222, 1998.

    MATH  MathSciNet  Google Scholar 

  5. R. Dechter. Bucket elimination: A unifying framework for reasoning. Artificial Intelligence, 113(1–2):41–85, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  6. R. Dechter and J. Pearl. Tree Clustering Schemes for Constraint Processing. In Proc. AAAI’ 88, 1988.

    Google Scholar 

  7. R. Dechter and 1. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In Proc. KR’ 94, pages 134–145. Morgan Kaufmann, 1994.

    Google Scholar 

  8. J. D.M. Gabbay, C.J. Hogger, editor. Handbook of Logic in Artzjicial Intelligence and Logic Programming, Vol. 3: Nonmonotonic Reasoning and Uncertain Reasoning. Oxford, 1993.

    Google Scholar 

  9. D. Etherington. Reasoning with incomplete Information. PhD thesis, University of British Columbia, 1986.

    Google Scholar 

  10. M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In 5th International Conference on Logic Programming, pages 1070–1080, 1988.

    Google Scholar 

  11. M. Gelfond and V. Lifschitz. Logic Program with Classical Negation. In D. H. D. Warren and P. Szeredi, editors, 7th Int. Conf. on Logic Programming, pages 579–597. MIT, 1990.

    Google Scholar 

  12. M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9, 1991.

    Google Scholar 

  13. W. Hodges. A shorter model theory. Cambridge U. Press, 1997.

    Google Scholar 

  14. T. Imielinski. Results on translating defaults to circumscription. Artificial Intelligence, 32(1): 131–146, Apr. 1987.

    Article  MATH  MathSciNet  Google Scholar 

  15. V. Lifschitz. Computing circumscription. In Proc. of IJCAI-85, pages 121–127, 1985.

    Google Scholar 

  16. V Lifschitz. Circumscription. In D. Gabbay, C.J. Hogger, and J.A. Robinson, editors, H.B. of Logic in Artificial Intelligence and Logic Programming, Vol. 3. Oxford U. Press, 1993.

    Google Scholar 

  17. V. Lifschitz and H. Turner. Splitting a logic program. In Proc. 11th Int’l Conf. on Logic Programming, pages 23–37. MIT Press, 1994.

    Google Scholar 

  18. V. M. Marek and M. Truszczynski. Nonmonotonic Logics; Context-Dependent Reasoning. Springer Verlag, Berlin-Heidelberg-NewYork, 1st edition, 1993.

    Google Scholar 

  19. J. McCarthy. Circumscription-A Form of Non-Monotonic Reasoning. Artificial Inteligence, 13:27–39, 1980.

    Article  MATH  MathSciNet  Google Scholar 

  20. J. McCarthy. Applications of Circumscription to Formalizing Common Sense Knowledge. Artificial Intelligence, 28:89–116, 1986.

    Article  MathSciNet  Google Scholar 

  21. S. McIlraith and E. Amir. Theorem proving with structured theories. In IJCAI’ 01, pages 624–631, 2001.

    Google Scholar 

  22. T. Przymusinski. Stable semantics for disjunctive programs. New Generation Computing, 9:401–424, 1991.

    Article  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  25. C. Sakama and K. Inoue. Relating disjunctive logic programs to default theories. In LP-NMR’ 93, pages 266–282, 1993.

    Google Scholar 

  26. H. Turner. Splitting a default theory. In Proc. AAAI’ 96, pages 645–651, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Amir, E. (2002). Interpolation Theorems for Nonmonotonic Reasoning Systems. In: Flesca, S., Greco, S., Ianni, G., Leone, N. (eds) Logics in Artificial Intelligence. JELIA 2002. Lecture Notes in Computer Science(), vol 2424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45757-7_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-45757-7_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44190-8

  • Online ISBN: 978-3-540-45757-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics