Missing Logtalk 2.19.0 files.

git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1108 b08c6af1-5177-4d33-ba66-4b1c6b8b522a

Logtalk/examples/logic/NOTES

@@ -0,0 +1,35 @@
+=================================================================
+Logtalk - Object oriented extension to Prolog
+Release 2.17.2
+
+Copyright (c) 1998-2004 Paulo Moura.  All Rights Reserved.
+=================================================================
+
+
+To load all entities in this example compile and load the loader file:
+
+| ?- logtalk_load(loader).
+
+This folder contains an object which implements a translator from 
+logic propositions to a set of clauses in conjunctive normal form. 
+The translator code is partially based on code published in the 
+book "Programming in Prolog" by W. F. Clocksin and C. S. Mellish.
+
+The following operators are used for representing logic connectives:
+
+	negation: ~
+	disjunction: v
+	conjunction: &
+	implication: =>
+	equivalence: <=>
+
+Quantifiers are represented using the following notation:
+
+	universal: all(X, P)
+	existential: exists(X, P)
+
+The two main object predicates are translate/2 and step_by_step/2.
+The first predicate, translate/2, translate a logic proposition to 
+a list of clauses. The second predicate, step_by_step/2, performs 
+the same translations as translate/2 but also prints the results 
+of each conversion step.

Logtalk/examples/logic/SCRIPT

@@ -0,0 +1,98 @@
+=================================================================
+Logtalk - Object oriented extension to Prolog
+Release 2.17.2
+
+Copyright (c) 1998-2004 Paulo Moura.  All Rights Reserved.
+=================================================================
+
+
+% start by loading the example:
+
+| ?- logtalk_load(loader).
+...
+
+
+% translate a single logic proposition:
+
+| ?- translator::translate((p v ~q) => (r & k), Cs).
+r :- p.
+k :- p.
+q; r :- .
+q; k :- .
+
+
+Cs = [cl([r],[p]),cl([k],[p]),cl([q,r],[]),cl([q,k],[])]
+yes
+
+
+% translate a single logic proposition printing each translation step:
+
+| ?- translator::step_by_step((p v ~q) => (r & k), Cs).
+
+Processing proposition: p v ~q=>r&k
+
+  1. Remove implications: ~ (p v ~q) v r&k
+  2. Distribute negation: ~p&q v r&k
+  3. Remove existential quantifiers: ~p&q v r&k
+  4. Convert to prenex normal form: ~p&q v r&k
+  5. Remove universal quantifiers: ~p&q v r&k
+  6. Convert to conjunctive normal form: (~p v r)&(~p v k)&((q v r)&(q v k))
+  7. Convert to clauses: [cl([r],[p]),cl([k],[p]),cl([q,r],[]),cl([q,k],[])]
+
+Clauses in Prolog-like notation:
+r :- p.
+k :- p.
+q; r :- .
+q; k :- .
+
+
+Cs = [cl([r],[p]),cl([k],[p]),cl([q,r],[]),cl([q,k],[])]
+yes
+
+
+% translate a single logic proposition printing each translation step:
+
+| ?- translator::step_by_step(all(X, exists(Y, p(X) v ~q(X) => r(X, Y))), Cs).
+
+Processing proposition: all(X, exists(Y, p(X)v~q(X)=>r(X, Y)))
+
+  1. Remove implications: all(X, exists(Y, ~ (p(X)v~q(X))v r(X, Y)))
+  2. Distribute negation: all(X, exists(Y, ~p(X)&q(X)v r(X, Y)))
+  3. Remove existential quantifiers: all(X, ~p(X)&q(X)v r(X, f1(X)))
+  4. Convert to prenex normal form: all(X, ~p(X)&q(X)v r(X, f1(X)))
+  5. Remove universal quantifiers: ~p(X)&q(X)v r(X, f1(X))
+  6. Convert to conjunctive normal form: (~p(X)v r(X, f1(X)))& (q(X)v r(X, f1(X)))
+  7. Convert to clauses: [cl([r(X, f1(X))], [p(X)]), cl([q(X), r(X, f1(X))], [])]
+
+Clauses in Prolog-like notation:
+r(X, f1(X)) :- p(X).
+q(X); r(X, f1(X)) :- .
+
+
+X = X
+Y = f1(X)
+Cs = [cl([r(X, f1(X))], [p(X)]), cl([q(X), r(X, f1(X))], [])] 
+yes
+
+
+% translate a single logic proposition printing each translation step:
+
+| ?- translator::step_by_step(all(X, men(X)  => mortal(X)), Cs).
+
+Processing proposition: all(X, men(X)=>mortal(X))
+
+  1. Remove implications: all(X, ~men(X)v mortal(X))
+  2. Distribute negation: all(X, ~men(X)v mortal(X))
+  3. Remove existential quantifiers: all(X, ~men(X)v mortal(X))
+  4. Convert to prenex normal form: all(X, ~men(X)v mortal(X))
+  5. Remove universal quantifiers: ~men(X)v mortal(X)
+  6. Convert to conjunctive normal form: ~men(X)v mortal(X)
+  7. Convert to clauses: [cl([mortal(X)], [men(X)])]
+
+Clauses in Prolog-like notation:
+mortal(X) :- men(X).
+
+
+X = X
+Cs = [cl([mortal(X)], [men(X)])] 
+yes