%============================================================================== % Project: SLP - An Interpreter for Super Logic Programs / Static Semantics % Module: testA.txt % Purpose: This is a test for hyperresolution (several steps, termination) % Last Change:12.10.2001 % Language: SLP % Author: Stefan Brass % Email: Stefan.Brass@informatik.uni-giessen.de, sbrass@sis.pitt.edu % Address: Universitaet Giessen, Arndtstr. 2, 35392 Giessen, Germany % Copyright: (c) 2001 by Stefan Brass % Licence: Distributed under the conditions of the GNU Public Licence. %============================================================================== % This is a test for the hyperresolution. % Disjunctions are not used, but the duplicate elimination and termination % are interesting. It is a "transitive closure" application. % The facts define a graph that looks as follows: % a -> b -> c -> d % ^ | % | | % +---------+ edge(a,b). edge(b,c). edge(c,d). edge(c,a). % The rules are the standard transitive closure rules % plus one rule that only generates duplicates: path(X,Y) :- edge(X,Y). path(X,Y) :- path(X,Y). path(X,Z) :- edge(X,Y), path(Y,Z). % The following facts should be derived: % Given facts: % edge(a,b). % edge(b,c). % edge(c,d). % edge(c,a). % First round: % path(a,b). % path(b,c). % path(c,d). % path(c,a). % Second round: % path(a,c). % path(b,d). % path(b,a). % path(c,b). % Third round: % path(a,d). % path(a,a). % path(b,b). % path(c,c). $v.