×

Interpolable formulas in equilibrium logic and answer set programming. (English) Zbl 1239.68069

A monotonic inference relation \(\vdash_L\) has the interpolation property if for all sentences \(\varphi\) and \(\psi\) with \(\vdash_L\varphi\rightarrow\psi\), there exists a sentence \(\xi\) built from function and predicate symbols that all occur in both \(\varphi\) and \(\psi\) such that \(\vdash_L\varphi\rightarrow\xi\) and \(\vdash_L\xi\rightarrow\psi\). This definition is inappropriate for a nonmonotonic inference relation \(\vsim\) because \(\vsim\varphi\rightarrow\xi\) and \(\vsim\xi\rightarrow\psi\) does not generally imply \(\vsim\varphi\rightarrow\psi\). Suppose that \(\vdash_L\) is a deductive base for \(\vsim\), that is, satisfies a number of conditions which, in particular, imply that \(\varphi\vsim\psi\) whenever \(\vsim\varphi\rightarrow\xi\) and \(\vdash_L\xi\rightarrow\psi\). Then the definition can be adapted to require that \(\vsim\varphi\rightarrow\xi\) and \(\vdash_L\xi\rightarrow\psi\), rather than \(\vsim\varphi\rightarrow\xi\) and \(\vsim\xi\rightarrow\psi\), hold whenever \(\vsim\varphi\rightarrow\psi\). The authors prove that this interpolation property is satisfied when \(\vsim\) is the relation of equilibrium entailment, where given a nonempty set \(\Pi\) of formulas having an equilibrium model, \(\Pi\vsim\varphi\) iff every equilibrium model of \(\Pi\) is a model of \(\varphi\). The notion of an equilibrium model is defined in the logic of here and there, whose semantics is based on Kripke frames with two worlds, here (\(h\)) and there (\(t\)) and satisfies the laws of intuitionistic logic, making it the strongest logic including intuitionistic logic and included in classical logic. An equilibrium model of \(\Pi\) is then such a Kripke frame with the property that \(h\) and \(t\) are the same structures, and the interpretation of relations in \(h\) cannot be made strictly smaller and still yield another model of \(\Pi\). The logic of here and there plays the role of deductive base for this choice of \(\vsim\). Two variants of \(\vsim\) are considered to deal with the case where the language is not fixed: \(\Pi\vsim_{ow}\varphi\) for the “open world” variant where the interpretation of logical symbols occurring in \(\varphi\) but not in \(\Pi\) is given after a minimal model of \(\Pi\) has been selected, and \(\Pi\vsim_{cw}\varphi\) for the “closed world” variant where it is not. Also, both the cases of propositional and static first-order equilibrium logic (with \(s\) and \(t\) sharing the same domain) are considered. Whereas the interpolation property holds in the propositional case, in the first order case, it is only shown to hold in case the collection of equilibrium models of \(\varphi\) is definable within the language. The definability restriction is shown not to be too restrictive in the case of a language with no function symbols besides constants where only safe formulas \(\varphi\) and \(\psi\) are considered – a notion which generalises the constraint that every variable that appears on the right hand side of an implication also occurs in the left hand side (having in mind to conceive of an implication as the rule of a logic program). The authors show how to apply their results to the answer set semantics thanks to \(\vsim_{cw}\), as well as to the notion of inseparable theories, that is, theories which produce the same answer sets for a given query language. Finally, they consider a stronger form of interpolation, namely, uniform interpolation where the same formula \(\xi\) has to be used for all formulas \(\psi\) sharing the same signature, and show that a uniform interpolation result can also be obtained.

MSC:

68T27 Logic in artificial intelligence
03B55 Intermediate logics
PDFBibTeX XMLCite
Full Text: arXiv