Decidability of Reasoning under the Well-Founded Semantics
Decidability of Reasoning under the Well-Founded Semantics
Master's thesis by Natalia Cherchago
- Supervisor Steffen Hölldobler
- Wissensverarbeitung
- 2010 – 2010
- Download
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.
