Volume 6: January - December 1996

Issue 5: October 1996


Generic models of logic programs

  • Generic models of logic programs
  • R. Sigal Department of Mathematics and Computer Science, State University of New York at New Paltz, New Paltz, NY 12561, USA


    The notion of minimal Herbrand models can be generalized to goal-generic models A, which have the property that P [vDash] [forall](L1 [and]...[and] Ln) iff A [vDash] [forall](L1 [and]...[and] Ln), where P is a program and <- L1,...,Ln 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 like Q = {p(0) <- ; q(0) <- [not]p(x); r(0) <- [not]q(0) } with no perfect model A such that, for all normal goals <- L1,...,Ln, PERF(Q) [vDash] [forall](L1 [and]...[and] Ln) iff A [forall](L1 [and]...[and] Ln). However, there do exist two models A, B such that PERF(Q) [vDash] [forall](L1 [and]...[and] Ln) iff {A,B} [vDash] [forall](L1 [and]...[and] Ln), suggesting the conjecture that all stratified programs 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 model A realizes a Cauchy term sequence T = tii[member of]N if there is some element in the domain of A which is an instance of every term in T, and A 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 program P which can determine if a model realizes any given computable Cauchy sequence, and show that P 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

    General Information

    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