%============================================================================== % Project: SLP - An Interpreter for Super Logic Programs / Static Semantics % Module: test9.txt % Purpose: This is a test for hyperresolution (single step) % Last Change:13.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. %============================================================================== % There is only a single rule: p(X) | q(X) :- r(a,X,_), s(X), not t(X). % This fact does not match the first body literal: r(b,b,b). % The second head literal of this conditional fact % matches the first body literal: q(a) | r(a,a,b) :- not t(c). % This also matches the first body literal: r(a,1,2) | q(2) :- not t(1). % This matches the first body literal, % but there is no corresponding match for the second body literal: r(a,2,2) :- not t(2). % Matches for the second body literal: s(a). q(3) | s(1) | q(4). % The following conditional facts must be derived: % Given facts: % r(b, b, b). % q(a) | r(a, a, b) :- not t(c). % r(a, 1, 2) | q(2) :- not t(1). % r(a, 2, 2) :- not t(2). % s(a). % q(3) | s(1) | q(4). % First Round: % p(a) | q(a) :- not t(a), not t(c). % p(1) | q(1) | q(2) | q(3) | q(4) :- not t(1). % The residual program is (in the sequence computed by the program): % r(b, b, b). % s(a). % q(3) | s(1) | q(4). % q(a) | r(a, a, b). % p(1) | q(1) | q(2) | q(3) | q(4). % r(a, 1, 2) | q(2). % r(a, 2, 2). % p(a) | q(a). $v.