Synonymous theories and knowledge representations in answer set programming

Even within a single knowledge representation system there are often many different ways to model a given domain and formalise a reasoning problem specified over the domain. In particular, two knowledge descriptions can be semantically equivalent even if they are expressed in quite different languages or vocabularies. This paper proposes and studies a concept of synonymy that applies to equivalent theories formulated in distinct vocabularies. We suggest a set of general desiderata or criteria of adequacy that any reasonable synonymy concept should satisfy. We then analyse a specific concept of synonymy within answer set programming (ASP), a framework that is currently being applied with success in many areas of knowledge technology. We characterise this concept in different ways, show that it satisfies the prescribed criteria of adequacy, and illustrate how it can be applied to a sample problem arising in knowledge representation and reasoning. As a logical framework we use quantified equilibrium logic based on a first-order version of the logic of here-and-there. This serves as an adequate formal foundation for ASP and allows us to obtain a logical account of the synonymy relation. (C) 2011 Elsevier Inc. All rights reserved.