Matpic
mathematics, in pictures
Concept

Literal

A variable, or the negation of a variable — the smallest piece from which a clause is built. Working in literals rather than in variables is what allows a single inference rule to cancel one variable between two clauses.

Named by 3 essays across one field — each of them below, with the objects they name alongside it.

A tableau for ((p → q) ∧ (q → r)) → (p → r). A branching tree of formulas, each branch ending in a contradiction or in a description of a counterexample.

The tree that closes

To prove a formula, assume it false and take it apart. Every branch ends in a contradiction, or one of them describes exactly how it could have been false — and either way the tree is the answer, drawn.

logic · Proof systems A resolution refutation of four clauses on three variables. A derivation tree: the given clauses at the top, each later clause obtained by cancelling one variable between two clauses above it, ending in the empty clause.

A proof with one rule

Two clauses that disagree about exactly one variable can be combined into a third that forgets it; repeat, and if the clauses cannot all be true the empty clause eventually appears — a complete proof system with a single move.

logic · Resolution 5 two-literal clauses drawn as 10 arrows. The literals of four variables arranged in a circle with an arrow for each implication a two-literal clause contains, the arrows forming a path from one literal to its negation and back highlighted, beside the list of clauses and their arrows.

Two literals make an arrow

A clause of two literals, p ∨ q, says that if p is false then q is true, and if q is false then p is true — two arrows. A set of such clauses is a directed graph on the literals, and it is unsatisfiable exactly when some variable and its negation reach each other. Each of those two paths is a chain of resolution steps, and finding them takes time proportional to the size of the input.

logic · Resolution

Named alongside it

The objects these essays reach for when they reach for this one.

RefutationSatisfiabilityCompletenessNormal formProof systemResolutionSoundnessBranchingDecision procedureGraphTableauThreshold

All concepts