Loop Formulas for Description Logic Programs

TL;DR

This paper extends the concepts of completion and loop formulas to description logic programs, introducing a new canonical answer set semantics that avoids circular justifications and enhances the formal understanding of dl-programs.

Contribution

It generalizes completion and loop formulas to dl-programs and proposes a canonical answer set semantics that eliminates circular justifications.

Findings

Answer sets are characterized by models of completion and loop formulas.

Canonical answer sets are free of circular justifications.

Properties of canonical answer sets are analyzed.

Abstract

Description Logic Programs (dl-programs) proposed by Eiter et al. constitute an elegant yet powerful formalism for the integration of answer set programming with description logics, for the Semantic Web. In this paper, we generalize the notions of completion and loop formulas of logic programs to description logic programs and show that the answer sets of a dl-program can be precisely captured by the models of its completion and loop formulas. Furthermore, we propose a new, alternative semantics for dl-programs, called the {\em canonical answer set semantics}, which is defined by the models of completion that satisfy what are called canonical loop formulas. A desirable property of canonical answer sets is that they are free of circular justifications. Some properties of canonical answer sets are also explored.