Backchaining
Backchaining is easily implemented as a recursive tree search (file backch.clj).
The function (backchain goal rules facts) tries to prove a goal given a set of rules and facts.
goal is a symbol (atom or propositional variable).
facts is a list of atoms that are known to be true.
rules is a list of rules of the form (conclusion prem1 ... premn ); each rule states that the conclusion is true if all of the premises are true.
For example, the rule A ∧ B → C would be written C ← A ∧ B or (c a b), similar to Prolog, c :- a,b .