An Abstract, Logical Approach to Characterizing Strong Equivalence in Non-monotonic Knowledge Representation Formalisms

VCLA and WPI hosting a talk by Ringo Baumann

ABSTRACT

Two knowledge bases are strongly equivalent if and only if they are mutually interchangeable in arbitrary contexts. This notion is of high interest for any logical formalism since it allows one to locally replace, and thus give rise for simplification, parts of a given theory without changing the semantics of the latter. In contrast to classical logic where strong equivalence coincides with standard equivalence (having the same models), it is possible to find ordinary but not strongly equivalent objects for any nonmonotonic formalism available in the literature. Consequently, much effort has been devoted to characterizing strong equivalence for knowledge representation formalisms such as logic programs, Reiter's default logic, or Dung's argumentation frameworks. For example, strong equivalence for logic programs under stable models can be characterized by so-called HT-models. More precisely, two logic programs are strongly equivalent if and only if they are standard equivalent in the logic here-and-there.

This means, the logic of here-and-there can be seen as a characterizing formalism for logic programs under stable model semantics. The aim of this article is to study whether the existence of such characterization logics can be guaranteed for any logic. One main result is that every knowledge representation formalism that allows for a notion of strong equivalence on its finite knowledge bases also possesses a canonical characterizing formalism. In particular, we argue that those characterizing formalisms can be seen as classical, monotonic logics.

Moreover, we will not only show the existence of characterizing formalism, but even that the model theory of any characterizing logic is uniquely determined (up to isomorphism).

CONTACT

Institute for Logic and Computation

Ringo Baumann, Leipzig University