Resolution

Enter formulas to test satisfiability, or premises and a conclusion separated by ∴ to test validity. For an inference, the search adds the negated conclusion to the premises and tries to derive the empty clause.

Scope. Propositional and first-order resolution. Each calculation begins by converting the input to clauses.

Propositional resolution

The search resolves complementary literals until it derives ⊥ or reaches saturation. Saturation establishes satisfiability without constructing a model; use truth tables to find a satisfying valuation.

Ex.

The interactive example is loading.

Choose the inferences

Select complementary literals in two clauses, then Resolve. The input is converted to CNF before you begin. Undo and Restart let you revise your choices; Saturated? checks whether every clause pair and pivot has been tried.

Choose a level to begin.

First-order resolution

Use closed formulas with explicit argument brackets. This calculus supports predicates and functions; identity requires additional rules. The search stops after at most 16 inferences. A stopped search without ⊥ leaves validity undecided.

Choose the inferences

Select two opposite-sign literals and choose Resolve. For Factor, select two same-sign literals in one clause. The unifier applies to the entire resulting clause. Undo removes the last inference; Restart returns to the input clauses. The workspace allows up to 80 clauses.

Using it

Separate premises with semicolons and put ∴ before the conclusion. Omit the conclusion to test satisfiability. Start the calculation, then use the step arrows to follow the search. The pencil unlocks the input for a new problem. Fullscreen makes room for wider first-order derivations.

Use normal forms , Skolemization , and unification to inspect the supporting calculations.

In the book