The homogeneous form of logic programs with equality.
William Demopoulos · Notre Dame Journal of Formal Logic · 1990
Let P be a Horn clause logic program.We suppose that P is symmetric in the sense that if C is a clause in P whose head is s = t, then there is a clause C* in P which is like C except for having the head t = s.The homogeneous form of a clausep(t x ,... ,t n ) <-B λ ,..., B q is p(x λ ,...,x n ) <-Xι = t x ,..., x n = t n , B λ ,..., B q .The homogeneous form P f of P is the set of homogeneous forms of clauses of P. Let 7" be a set of axioms asserting the reίlexivity, symmetry, transitivity, and congruence (with respect to the predicates of P) of =.Then PUT is goal equivalent to P' U [x = x) i.e., for any goal G, PU TU [G] is unsatisfiable iff P' U{x = x}U[G}is unsatisfiable.The main interest of the paper lies in its construction of the Herbrand model M and in the proof that Mis the minimal Herbrand model of both P U Γand P'U {x = x}. DefinitionLet P be a program.The homogeneous form P' of P is the set of homogeneous forms of the clauses in P.