Propositional Prolog · SLD resolution

Backward chaining

The engine starts from the goal and works back towards the facts. At each node it selects the leftmost goal and resolves it with every clause whose head matches, trying those clauses top to bottom and searching depth first. A branch that empties the goal list is a proof. Press Next after a proof to backtrack and look for the next one.

SLD resolution tree

Ready 0 proofs

Program

Current node
Untried alternative
Current branch
Proof branch
Fails: no matching clause
Cut off at the depth limit

Ready

Edit program

Write clauses in Prolog notation, each ending with a period: rules as head :- a, b. and facts as a. Atoms start with a lowercase letter. Text after % is a comment. Applying resets the search.