NAF-Based Logic Semantics: Proof-Theoretic Generalization and Non-Ground Extension
Salazar, Elmer E
MetadataShow full item record
There are several semantics based for negation as failure in logic programming. These semantics can be realized with a combination of induction and coinduction, and this realization can be used to develop a goal-directed method of computing models. In essence, the difference between these semantics is how they resolve the unstratified portions of a program. Two major, but related, topics are covered. Firstly, while being restricted to the propositional case, we show how a semantics is a mixture of induction and coinduction, and how we can use coinduction to resolve the cycles formed by the rules in a program. We present denotational semantics based on a fixed point of a function, and show its equivalence to the use of induction and coinduction. We take a look at the different ways a semantics may resolve cycles, and show how to implement two popular semantics, well-founded and stable models, as well as costable model semantics. Finally, we present operational semantics as a parametrized goal-directed algorithm that allows us to determine how cycles are resolved. Secondly, a Method for computing stable models of normal logic programs, i.e., logic programs extended with negation, in the presence of predicates with arbitrary terms will be presented. Such programs need not have a finite grounding, so traditional methods do not apply. This method relies on the use of a non-Herbrand universe, as well as coinduction, constructive negation and a number of other novel techniques. Using this method, a normal logic program with predicates can be executed directly under the stable model semantics without requiring it to be grounded either before or during execution and without requiring that its variables range over a finite domain. As a result, the method is quite general and supports the use of terms as arguments, including lists and complex data structures.