Propositional logic: truth tables, clausal form and resolution

“If the sensor is triggered and there is no guard, the alarm goes off.” “Someone is Spanish only if they are European.” Is if (a < b || (a >= b && c == d)) the same as if (a < b || c == d)? All three hide the same question: what follows from what. Propositional logic is the simplest tool for answering it, and the foundation of logic programming, software verification, digital circuits and a good part of artificial intelligence.

​

What you will learn

• Translate sentences from natural language into formulas, including the tricky ones (“only if”, “is necessary for”, “unless”).
• Read a formula using the precedence of the connectives and evaluate it under an interpretation.
• Classify formulas as valid, satisfiable or unsatisfiable, and sets of formulas as consistent or inconsistent.
• Decide whether an argument is valid with a truth table.
• Convert any formula into conjunctive normal form and clausal form.
• Prove an argument by resolution, deriving the empty clause.

​

How to use the simulator

The simulator’s interface is in Spanish. The table gives each control’s Spanish label.

• With premises and a conclusion, the simulator says whether the argument is valid and, if it is not, gives a counterexample.
• With a single formula, it classifies it: valid, satisfiable or unsatisfiable.
• With several formulas and no conclusion, it says whether the set is consistent.
• Propositions are lowercase letters (p, q, r, p1…). The constants true and false are written V and F, from the Spanish verdadero and falso.

​

Theory

​

Propositions and connectives

A proposition is the smallest piece of information that can be said to be true or false: “it is raining”, “John is a doctor”. Questions, exclamations and sentences whose truth depends on a variable (”$X$ is greater than 3”) are not propositions; the last ones belong to predicate logic. Propositions are combined with five connectives:

​

Syntax and precedence

Well-formed formulas are built from the atomic ones (the propositions and the constants $V$ and $F$): if $F$ and $G$ are formulas, so are $\lnot F$, $(F \land G)$, $(F \lor G)$, $(F \to G)$ and $(F \leftrightarrow G)$. To save brackets, connectives have a precedence, from highest to lowest: $$\lnot \quad > \quad \land \quad > \quad \lor \quad > \quad \to \quad > \quad \leftrightarrow$$ So $\lnot p \land q \to r$ reads $((\lnot p \land q) \to r)$. Between connectives of the same level, the leftmost one goes first: $p \to q \to r$ is $(p \to q) \to r$. The simulator writes those brackets even when they are not needed, because the formula is hard to read without them.

​

Semantics: interpretations and truth tables

An interpretation assigns true (V) or false (F) to each proposition. With $n$ different propositions there are $2^n$ interpretations. The value of a formula is computed with the tables of the connectives: The conditional is false in only one case: true antecedent and false consequent. If the antecedent is false, the conditional is true (“anything follows from a falsehood”). An interpretation that makes a formula true is a model of it; one that makes it false, a countermodel.

​

Classifying formulas

Every valid formula is satisfiable. The two classes are linked by the mirror principle: $$F \text{ is valid} \iff \lnot F \text{ is unsatisfiable}$$ A set of formulas is consistent if a single interpretation makes all of them true, and inconsistent if there is none. Careful: $\{p,\ \lnot p\}$ is inconsistent even though each formula on its own is satisfiable.

​

Logical equivalence

Two formulas are equivalent, $F \equiv G$, if they have the same value under every interpretation, that is, if $F \leftrightarrow G$ is valid. The most useful equivalences:

​

Logical consequence: when an argument is valid

$Q$ is a logical consequence of the premises $P_1, \dots, P_n$, written $\{P_1, \dots, P_n\} \models Q$, if every common model of the premises is also a model of $Q$. An argument is valid when its conclusion is a logical consequence of its premises. There are two equivalent ways to check it: $$\textbf{Theorem I:}\quad \{P_1, \dots, P_n\} \models Q \iff P_1 \land \dots \land P_n \to Q \text{ is valid}$$ $$\textbf{Theorem II:}\quad \{P_1, \dots, P_n\} \models Q \iff \{P_1, \dots, P_n, \lnot Q\} \text{ is inconsistent}$$ The truth table uses Theorem I: look for the rows where every premise is true and check the conclusion. If it is false in any of them, that row is a counterexample and the argument is not valid. The method always works, but with $n$ propositions there are $2^n$ rows: with 10 there are already 1024.

​

Conjunctive normal form and clausal form

A literal is a proposition or its negation; $L^c$ is its complement ($p$ and $\lnot p$). A formula is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals, such as $(p \lor \lnot q) \land (\lnot p \lor r \lor s) \land p$. Each disjunction is a clause, and the set of clauses is the clausal form. The clause with no literals is the empty clause $\square$, which is unsatisfiable. Any formula can be converted to CNF in five steps, the same ones the simulator shows:

​

Resolution

Resolution (Robinson, 1965) uses a single inference rule, which is very easy to automate: $$\frac{L \lor F \qquad L^c \lor G}{F \lor G}$$ A pair of complementary literals is removed and what is left of the two clauses is joined: the result is the resolvent. It works because, if $L$ is false, $F$ has to be true, and if $L$ is true, $G$ has to be true; either way, $F \lor G$ holds. To prove an argument, you work by refutation, using Theorem II:

1. Convert the premises and the negation of the conclusion to clausal form.
2. Resolve pairs of clauses and add the resolvents.
3. If the empty clause $\square$ appears, the set is inconsistent and the argument is valid.
4. If every possible pair has been resolved without reaching $\square$, the set is consistent and the argument is not valid.

The simulator tries every pair level by level (each new clause against all the earlier ones), discards tautologies and absorbed clauses, and finally shows only the resolvents that lead to $\square$.

​

Worked examples

​

Try it in the simulator

​

Common mistakes

• Translating “p only if q” as $q \to p$. It is $p \to q$.
• Thinking that $p \to q$ is false when $p$ is false. It is only false when $p$ is true and $q$ is false.
• Confusing satisfiable with valid. A formula being true in some row does not make it a tautology.
• Forgetting to negate the conclusion before resolving. Resolving with $Q$ instead of $\lnot Q$ proves nothing.
• Resolving on two pairs at once. $p \lor q$ and $\lnot p \lor \lnot q$ do not give $\square$: each resolution step removes a single pair, and here any resolvent is a tautology.
• Distributing the wrong way. For CNF you distribute $\lor$ over $\land$, not $\land$ over $\lor$ (that gives the disjunctive normal form).

​

Limitations

Propositional logic cannot talk about objects or their properties. “All men are mortal; Socrates is a man; therefore Socrates is mortal” is a valid argument that cannot be proved here: it needs the quantifiers ($\forall$, $\exists$) of predicate logic. Besides, deciding whether a formula is satisfiable (the SAT problem) is NP-complete: no known method does it in polynomial time. Truth tables grow as $2^n$ and resolution can generate a huge number of clauses. The simulator draws tables of up to 7 propositions and stops at 3000 clauses. Even so, modern SAT solvers handle industrial problems with millions of variables.

​

A bit of history

Aristotle studied syllogisms in the 4th century BC, but logic as a calculus starts with George Boole, who in 1854 treated propositions with the rules of algebra. Gottlob Frege gave the first complete formal system in 1879. In 1935 Gerhard Gentzen proposed natural deduction, which mimics how people reason, and in 1965 John Alan Robinson invented resolution, designed for machines to reason. It led to the Prolog language (1972), which runs programs by resolving Horn clauses.

​

Frequently asked questions

​

Related simulators

These simulators and their notes are in Spanish.