Forward and backward chaining

Enter facts, rules, and a query, then follow how forward or backward chaining tries to establish the query. Compare the facts each search visits.

Scope. Propositional definite clauses and an atomic query. Rule bodies may contain conjunctions; each rule has one positive atomic head.

Choose a direction

The example is loading.

Derivations found

Compare searches

The example is loading.

Derivations found

Using it

Enter one fact or rule per line, such as RAIN or (RAIN ∧ SUN) → RAINBOW, and an atom in the query field. Start the search, then use the arrows to inspect its steps. The comparison has separate step controls for forward rounds and backward depth-first search.

For Horn clauses that can express contradictions, use Horn satisfiability .

In the book