add examples from the power of prolog

src/prolog/examples/expert_system.pl

@@ -0,0 +1,42 @@
+:- use_module(library(dcgs)).
+:- use_module(library(reif)).
+
+animals([animal(dog, [is_true('has fur'), is_true('says woof')]),
+         animal(cat, [is_true('has fur'), is_true('says meow')]),
+         animal(duck, [is_true('has feathers'), is_true('says quack')])]).
+
+animal(A) :-
+    animals(Animals),
+    Known0 = [],
+    phrase(any_animal(Animals, A), [Known0], _).
+
+any_animal([Animal|Animals], A) -->
+    any_animal_(Animal, Animals, A).
+
+any_animal_(animal(A0, []), Animals, A) -->
+    (   { A0 = A }
+    ;   any_animal(Animals, A)
+    ).
+any_animal_(animal(A0, [C|Cs]), Animals, A) -->
+    state0_state(Known0, Known),
+    { condition_truth(C, T, Known0, Known) },
+    next_animal(T, animal(A0,Cs), Animals, A).
+
+next_animal(yes, Animal, Animals, A)  --> any_animal([Animal|Animals], A).
+next_animal(no, _, Animals, A)        --> any_animal(Animals, A).
+
+state0_state(S0, S), [S] --> [S0].
+
+condition_truth(is_true(Q), Answer, Known0, Known) :-
+    if_(known_(Q,Answer,Known0),
+        Known0 = Known,
+        ( writeq([Q, ?]), nl,
+	  read(Answer),
+          Known = [known(Q,Answer)|Known0])).
+
+known_(What, Answer, Known, Truth) :-
+    if_(memberd_t(known(What,yes), Known),
+        ( Answer = yes, Truth = true ),
+        if_(memberd_t(known(What,no), Known),
+            ( Answer = no, Truth = true),
+            Truth = false)).

src/prolog/examples/plres.pl

@@ -0,0 +1,54 @@
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+   Written by Markus Triska, triska@metalevel.at, Sept. 5th 2006
+   Public domain code.
+   ----------------------------------------------------------------------
+
+   Resolution calculus for propositional logic.
+
+   For more information about theorem proving with Prolog, see:
+
+   https://www.metalevel.at/prolog/theoremproving
+   ==============================================
+
+   Input is a formula in conjunctive normal form, represented as a
+   list of clauses; clauses are lists of atoms and terms not/1.
+
+   Example:
+
+   ?- Clauses = [[p,not(q)], [not(p),not(s)], [s,not(q)], [q]],
+      pl_resolution(Clauses, Rs),
+      maplist(portray_clause, Rs).
+   %@ [p, not(q)]-[not(p), not(s)] -->
+   %@   [not(q), not(s)].
+   %@ [s, not(q)]-[not(q), not(s)] -->
+   %@   [not(q)].
+   %@ [q]-[not(q)] -->
+   %@   [].
+
+   Iterative deepening is used to find a shortest refutation.
+
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
+
+:- use_module(library(dcgs)).
+:- use_module(library(dif)).
+:- use_module(library(lists)).
+
+pl_resolution(Clauses0, Chain) :-
+        maplist(sort, Clauses0, Clauses), % remove duplicates
+        length(Chain, _),
+        pl_derive_empty_clause(Chain, Clauses).
+
+pl_derive_empty_clause([], Clauses) :-
+        member([], Clauses).
+pl_derive_empty_clause([C|Cs], Clauses) :-
+        pl_resolvent(C, Clauses, Rs),
+        pl_derive_empty_clause(Cs, [Rs|Clauses]).
+
+pl_resolvent(((As0-Bs0) --> Rs), Clauses, Rs) :-
+        member(As0, Clauses),
+        member(Bs0, Clauses),
+        select(Q, As0, As),
+        select(not(Q), Bs0, Bs),
+        append(As, Bs, Rs0),
+        sort(Rs0, Rs), % remove duplicates
+        maplist(dif(Rs), Clauses).