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 ===== | ||
| + | <code prolog> | ||
| + | % 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, _). | ||
| + | </code> | ||
| + | ===== Comments ===== | ||
