Concept animations

These animations keep formulas and clauses visible as they change, making it easier to follow each transformation and inference step. Use the video timeline to pause, replay, or inspect any step.

CNF conversion

The animation follows a formula through the main stages of conversion to clausal normal form: eliminating implications, moving negations inward, standardizing variables, moving quantifiers, Skolemizing, dropping universal quantifiers, and distributing disjunctions.

A complete, step-by-step conversion to clausal normal form.

First-order resolution

The animation shows how two complementary literals are unified and resolved. Color and motion connect the most general unifier, the selected literals, and the resulting resolvent.

First-order resolution with the substitution and resolvent kept in view.

Given-clause selection

The animation follows clauses through the processed and unprocessed sets of a simplified saturation loop. It highlights the selected given clause, generated consequences, and the repeated search cycle.

A visual model of processed and unprocessed clauses during proof search.