Horn Clause Rule Engine

Enter facts and positive Horn rules, then prove a goal or derive all consequences. Each fact or rule occupies one line; a final period is optional. Blank lines and lines starting with # are ignored.

Use names such as parent(bob,ann). Variables start with an uppercase letter or underscore: ancestor(X,Z) :- parent(X,Y), ancestor(Y,Z). Each _ matches independently. Names are case-sensitive; constants and predicate names start with a lowercase letter. Functions, quoted or numeric constants, arithmetic and negation are not supported. Facts must be ground; every head variable must occur in the body.

Queries may contain variables: ancestor(dora,X) lists matching facts. Not proved means no answer follows from this knowledge base, not that the goal is false in the real world. The trace shows the first derivation of each new fact, its concrete premises and the inference round. Already-known facts do not produce another trace row. Open Known facts to inspect the complete current set.

Small, browser-only Datalog demonstrator: at most 12,000 characters per field, 300 fact lines, 100 rules, 8 arguments per atom and 12 premises per rule. Evaluation stops after 200 rounds, 1,000 known facts or 50,000 candidate comparisons. Partial results retain valid derived facts; missing answers are undecided.

Datalog rule grounding

Only input values are remembered in this browser. Calculated results and experiment histories are not saved.