R .Sigal Department of Mathematics and Computer Science, State University of New York at New Paltz, New Paltz , NY 12561,USA

ABSTRACT The notion of minimal Herbrand models can be generalized to goal-generic models

A , which have the property thatP [vDash] [forall](L 1 [and]...[and]L ) iffn A [vDash] [forall](L 1 [and]...[and]L ), wheren P is a program and <-L 1 ,...,L is a goal. In the first part of this paper we characterize a large class of goal-generic models for definite Horn programs. These are minimal models which satisfy Clark's Equality Theory and which contain an infinite number of 'unnamed' elements. Predictably, the situation deteriorates when negation is allowed. There are simple stratified programs liken Q = {p (0) <- ;q (0) <- [not]p(x) ;r (0) <- [not]q (0) } with no perfect modelA such that, for all normal goals <-L 1 ,...,L , PERF(n Q ) [vDash] [forall](L 1 [and]...[and]L ) iffn A [forall](L 1 [and]...[and]L ). However, there do exist two modelsn A, B such that PERF(Q ) [vDash] [forall](L 1 [and]...[and]L ) iff {n A,B } [vDash] [forall](L 1 [and]...[and]L ), suggesting the conjecture that all stratified programsn P have finite goal-generic models sets in PERF(P ). In the second part of this paper we show that this conjecture is false. The proof depends on a characterization of model domain elements by way of Cauchy term sequences, a finitary treatment of infinite terms. A modelA realizes a Cauchy term sequenceT =t i i [member of] if there is some element in the domain ofN A which is an instance of every term inT , andA omits T otherwise. Basic results from model theory show that the models of Clark's equality Theory display a rich variety in their realization and omission of Cauchy term sequences. We give a programP which can determine if a model realizes any given computable Cauchy sequence, and show thatP is a counterexample to the conjecture.

Keywords: Logic programming, semantics, equality theories, model theory, computable functions.

Pages:

629 -661

Part of the OUP Journal of Logic and Computation WWW service

Click here to register with OUP.

This page is maintained by OUP admin

Last updated 19 Nov 96

Part of the OUP Journals World Wide Web service.

Copyright Oxford University Press, 1996