Epistemic Logic Programs with Sorts

ABSTRACT. An epistemic logic program is a program written in the language of Epistemic Specifications, an extension of the language of answer set programming (ASP) that allows for introspective reasoning through the use of modal operators K and M. The language of Epistemic Specifications was introduced by Gelfond in the early 1990s after observing the need for a more powerful form of introspective reasoning than that offered by ASP alone. The semantics of an epistemic logic program was given in terms of its world view--a collection of sets of literals (belief sets), analogous to the answer sets of an ASP program. In 2011, Gelfond proposed a change to the semantics in a preliminary attempt to avoid certain unintended world views. Gelfond, Kahl, Watson, and Zhang continued this work in the hopes of finding a semantics that was satisfactory with respect to intuition and modeling of problems for which the added power of Epistemic Specifications showed promise.

Concurrent with this latter work was an effort by Balai, Gelfond, and Zhang to enhance ASP by providing a framework for specifying sorts for the parameters of predicates in a language they called SPARC. This promoted better program design, helped to eliminate certain common errors (e.g., misspellings), and encouraged development of rules specific to a particular domain without the concern for rule safety that has been associated with variable terms by popular ASP solvers (e.g., clingo, DLV).

In this paper, we combine these recent efforts by providing within the language of Epistemic Specifications a framework for specifying predicate parameter domains. We call a program written in this new language an epistemic logic program with sorts (ELPS). In addition to the benefits a sorted signature provides to the programmer, it also allows for a straightforward algorithm for computing world views. We describe such an algorithm--one that can take advantage of existing state-of-the-art ASP solvers--and give a synopsis of test results from our implementation. We conclude with a discussion of related work and a brief summary.