Interpolation Theorems for Nonmonotonic Reasoning Systems

TL;DR

This paper extends Craig's interpolation theorem to nonmonotonic reasoning systems like circumscription, default logic, and answer set programming, enhancing understanding and potential reasoning efficiency in these logics.

Contribution

It introduces interpolation theorems for three nonmonotonic systems, revealing underlying monotonicity principles and enabling structured reasoning and decomposition methods.

Findings

Interpolation theorems established for circumscription, default logic, and answer set semantics.

Results suggest some monotonicity principles hold despite nonmonotonicity.

Potential for improved reasoning decomposition and structured representations.

Abstract

Craig's interpolation theorem (Craig 1957) is an important theorem known for propositional logic and first-order logic. It says that if a logical formula $\beta$ logically follows from a formula $\alpha$, then there is a formula $\gamma$, including only symbols that appear in both $\alpha,\beta$, such that $\beta$ logically follows from $\gamma$ and $\gamma$ logically follows from $\alpha$. 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 \emph{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.