An abstract, logical approach to characterizing strong equivalence in non-monotonic knowledge representation formalisms

摘要

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 to locally replace parts of a given theory without changing its meaning. 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 under the stable model semantics, 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 of here and there. This means that the logic of here and there can be seen as a characterizing formalism for logic programs under stable model semantics.