# Różnice

Różnice między wybraną wersją a wersją aktualną.

 — pl:prolog:pllib:theorem_proving [2019/06/27 15:50] (aktualna) Linia 1: Linia 1: + ====== Theorem proving ====== + {{tag>​proof operators}} + ===== Description ===== + A pattern-directed program for simple resolution theorem proving. + + **Source**: ​ PROLOG programming for artificial intelligence,​ 3rd Edition, Harlow, 2001, ISBN 0-201-40375-7. + ===== Download ===== + Program source code: {{theorem_proving.pl}} + ===== Listing ===== + + %  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, _). + ​ + ===== Comments =====
pl/prolog/pllib/theorem_proving.txt · ostatnio zmienione: 2019/06/27 15:50 (edycja zewnętrzna)