Różnice między wybraną wersją a wersją aktualną.
| — |
pl:prolog:pllib:propositional_calculus_2_clauses [2019/06/27 15:50] (aktualna) |
||
|---|---|---|---|
| Linia 1: | Linia 1: | ||
| + | ====== Propositional calculus 2 clauses ====== | ||
| + | {{tag>operators logic}} | ||
| + | ===== Description ===== | ||
| + | Translating a propositional calculus formula into a set of (asserted) clauses. | ||
| + | |||
| + | **Source**: PROLOG programming for artificial intelligence, 3rd Edition, Harlow, 2001, ISBN 0-201-40375-7. | ||
| + | ===== Download ===== | ||
| + | Program source code: {{propositional_calculus_2_clauses.pl}} | ||
| + | ===== Listing ===== | ||
| + | <code prolog> | ||
| + | % Figure 23.16 Translating a propositional calculus formula into | ||
| + | % a set of (asserted) clauses. | ||
| + | |||
| + | |||
| + | % Translating a propositional formula into (asserted) clauses | ||
| + | |||
| + | :- op( 100, fy, ~). % Negation | ||
| + | :- op( 110, xfy, &). % Conjunction | ||
| + | :- op( 120, xfy, v). % Disjunction | ||
| + | :- op( 130, xfy, =>). % Implication | ||
| + | |||
| + | % translate( Formula): translate propositional Formula | ||
| + | % into clauses and assert each resulting clause C as clause( C) | ||
| + | |||
| + | translate( F & G) :- % Translate conjunctive formula | ||
| + | !, % Red cut | ||
| + | translate( F), | ||
| + | translate( G). | ||
| + | |||
| + | translate( Formula) :- | ||
| + | transform( Formula, NewFormula), % Transformation step on Formula | ||
| + | !, % Red cut | ||
| + | translate( NewFormula). | ||
| + | |||
| + | translate( Formula) :- % No more transformation possible | ||
| + | assert( clause( Formula)). | ||
| + | |||
| + | % Transformation rules for propositional formulas | ||
| + | |||
| + | % transform( Formula1, Formula2) if | ||
| + | % Formula2 is equivalent to Formula1, but closer to clause form | ||
| + | |||
| + | transform( ~(~X), X). % Eliminate double negation | ||
| + | |||
| + | transform( X => Y, ~X v Y). % Eliminate implication | ||
| + | |||
| + | transform( ~ (X & Y), ~X v ~Y). % De Morgan's law | ||
| + | |||
| + | transform( ~ (X v Y), ~X & ~Y). % De Morgan's law | ||
| + | |||
| + | transform( X & Y v Z, (X v Z) & (Y v Z)). % Distribution | ||
| + | |||
| + | transform( X v Y & Z, (X v Y) & (X v Z)). % Distribution | ||
| + | |||
| + | transform( X v Y, X1 v Y) :- | ||
| + | transform( X, X1). % Transform subexpression | ||
| + | |||
| + | transform( X v Y, X v Y1) :- | ||
| + | transform( Y, Y1). % Transform subexpression | ||
| + | |||
| + | transform( ~ X, ~ X1) :- | ||
| + | transform( X, X1). % Transform subexpression | ||
| + | </code> | ||
| + | ===== Comments ===== | ||
