Horn satisfiability

Check whether a collection of Horn clauses is satisfiable. The trace shows which facts enter the agenda and when a rule’s premises have all been met.

Scope. Propositional Horn clauses: facts, definite rules, and clauses with no positive literal. A rule may have ⊥ as its head.

The example is loading.

Derivations found

Using it

Enter one fact, rule, or clause per line. For example, RAIN, RAIN → WET, and WET → ⊥ form an unsatisfiable knowledge base. Start the calculation and step through the counters and agenda. The result reports whether a contradiction was reached.

Use chaining to follow a particular atomic query.

In the book