Decidability of Reasoning under the Well-Founded Semantics

From International Center for Computational Logic
Toggle side column

Decidability of Reasoning under the Well-Founded Semantics

Master's thesis by Natalia Cherchago
In this thesis we investigate issues concerning decidability of reasoning under the

well-founded semantics. First, we give an overview of meta-level properties of the well-founded semantics. We also define a new property—we call it the maximal path property. It tells us that the number of WP -iterations in the well-founded model computation is limited by the cardinality of the longest dependency path in the atom-call graph of the program.
We propose a new setting for analysis of decidability of logic programs. We focus our attention on properties of query atoms and their relevant subprograms rather than on a logic program as a whole. Our observation is that within a logic program P various atoms in its Herbrand base can have various properties, for example, finiteness of the dependency relation or length of the maximal dependency path. Within a single program P different query atoms have different relevant subprograms and thus yield different decidability results. We divide a Herbrand base of a logic program P into two subsets with respect to the cardinality of an atom dependency relation. Analysis of the meta-properties and their combination leads us to the definition of three classes of atoms with decidable query evaluation: finitely recursive, ω-recursive and ω-restricted atoms. Finitely recursive atoms with a finite dependency relation enjoy decidability of query evaluation because their relevant subprograms are finite; ω-recursive atoms have an infinite dependency relation, nevertheless they are decidable because their value can be computed in finite time due to the maximal path property; ω-restricted atoms have relevant subprograms with a certain syntactic restriction that allows for model computation to be a 2-NEXP-complete problem.