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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. Amir. (De)composition of situation calculus theories. In Proc. AAAI’ 00, pages 456–463. AAAI Press/MIT Press, 2000.
E. Amir and S. McIlraith. Paritition-based logical reasoning. In Proc. KR’ 2000, pages 389–400, 2000.
W. Craig. Linear reasoning. a new form of the Herbrand-Gentzen theorem. J. of Symbolic Logic, 22:250–268, 1957.
A. Darwiche. Model-based diagnosis using structured system descriptions. Journal of AI Research, 8: 165–222, 1998.
R. Dechter. Bucket elimination: A unifying framework for reasoning. Artificial Intelligence, 113(1–2):41–85, 1999.
R. Dechter and J. Pearl. Tree Clustering Schemes for Constraint Processing. In Proc. AAAI’ 88, 1988.
R. Dechter and 1. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In Proc. KR’ 94, pages 134–145. Morgan Kaufmann, 1994.
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.
D. Etherington. Reasoning with incomplete Information. PhD thesis, University of British Columbia, 1986.
M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In 5th International Conference on Logic Programming, pages 1070–1080, 1988.
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.
M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9, 1991.
W. Hodges. A shorter model theory. Cambridge U. Press, 1997.
T. Imielinski. Results on translating defaults to circumscription. Artificial Intelligence, 32(1): 131–146, Apr. 1987.
V. Lifschitz. Computing circumscription. In Proc. of IJCAI-85, pages 121–127, 1985.
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.
V. Lifschitz and H. Turner. Splitting a logic program. In Proc. 11th Int’l Conf. on Logic Programming, pages 23–37. MIT Press, 1994.
V. M. Marek and M. Truszczynski. Nonmonotonic Logics; Context-Dependent Reasoning. Springer Verlag, Berlin-Heidelberg-NewYork, 1st edition, 1993.
J. McCarthy. Circumscription-A Form of Non-Monotonic Reasoning. Artificial Inteligence, 13:27–39, 1980.
J. McCarthy. Applications of Circumscription to Formalizing Common Sense Knowledge. Artificial Intelligence, 28:89–116, 1986.
S. McIlraith and E. Amir. Theorem proving with structured theories. In IJCAI’ 01, pages 624–631, 2001.
T. Przymusinski. Stable semantics for disjunctive programs. New Generation Computing, 9:401–424, 1991.
R. Reiter. A logic for default reasoning. Artificial Intelligence, 13 (1–2):81–132, 1980.
V. Risch and C. Schwind. Tableau-based characterization and theorem proving for default logic. Journal of Automated Reasoning, 13:223–242, 1994.
C. Sakama and K. Inoue. Relating disjunctive logic programs to default theories. In LP-NMR’ 93, pages 266–282, 1993.
H. Turner. Splitting a default theory. In Proc. AAAI’ 96, pages 645–651, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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