% Figure 23.15 A pattern-directed program for simple resolution % theorem proving. :- op( 900, fy, not). :- op( 800, xfx, --->). :- op( 120, xfy, v). :- op( 100, fy, ~). % Negation % not Goal): negation as failure; % Note: This is often available as a built-in predicate, % often written as prefix operator "\+", e.g. \+ likes(mary,snakes) not Goal :- Goal, !, fail ; true. % The following directive is required by some Prologs :- dynamic clause/1, done/3. % Production rules for resolution theorem proving % Contradicting clauses [ clause( X), clause( ~X) ] ---> [ write('Contradiction found'), stop]. % Remove a true clause [ clause( C), in( P, C), in( ~P, C) ] ---> [ retract( C) ]. % Simplify a clause [ clause( C), delete( P, C, C1), in( P, C1) ] ---> [ replace( clause( C), clause( C1)) ]. % Resolution step, a special case [ clause( P), clause( C), delete( ~P, C, C1), not done( P, C, P) ] ---> [ assert( clause( C1)), assert( done( P, C, P)) ]. % Resolution step, a special case [ clause( ~P), clause( C), delete( P, C, C1), not done( ~P, C, P) ] ---> [ assert( clause( C1)), assert( done( ~P, C, P)) ]. % Resolution step, general case [ clause(C1), delete( P, C1, CA), clause(C2), delete( ~P, C2, CB), not done( C1,C2,P) ] ---> [ assert( clause(CA v CB)), assert( done( C1, C2, P)) ]. % Last rule: resolution process stuck [] ---> [ write('Not contradiction'), stop]. % delete( P, E, E1) if % deleting a disjunctive subexpression P from E gives E1 delete( X, X v Y, Y). delete( X, Y v X, Y). delete( X, Y v Z, Y v Z1) :- delete( X, Z, Z1). delete( X, Y v Z, Y1 v Z) :- delete( X, Y, Y1). % in( P, E) if P is a disjunctive subexpression in E in( X, X). in( X, Y) :- delete( X, Y, _).