Propositional Horn clauses

Forward chaining

The reasoner copies every fact into the closure, then works in iterations. Each iteration checks the body of every rule against the closure. When a whole body is satisfied, the rule fires and its head joins the closure. The reasoner stops after an iteration that adds nothing.

Not yet shown true
Being checked
Not in the closure
In the closure

Ready

Edit knowledge base

One clause per line. Write rules as A ^ B => C and facts as a single atom. Lines starting with # are ignored. Applying resets the animation.