--- /dev/null
+:- 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)).
--- /dev/null
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+ 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).