> ## Documentation Index
> Fetch the complete documentation index at: https://apuntes.simulab.es/llms.txt
> Use this file to discover all available pages before exploring further.

# Propositional logic: truth tables, clausal form and resolution

> Propositional logic explained: connectives, truth tables, valid and satisfiable formulas, logical consequence, conjunctive normal form and resolution, with worked examples.

<Card title="Open the simulator" icon="flask" href="https://simulab.es/matematicas/logica-proposicional">
  Type the premises and the conclusion and check the argument with a truth table, the clausal form and resolution. The simulator is in Spanish.
</Card>

"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.

| Control | What it does |
| - | - |
| **Premisas** (premises) | One formula per line (you can also separate them with `;`) |
| **Conclusión** (conclusion) | Optional. If empty, only the premises are studied |
| **Buttons ¬ ∧ ∨ → ↔ ( )** | Insert the symbol at the cursor. You can also type `~ & \| -> <->` |
| **Examples** | Load arguments from class and from the lab sessions |
| **Tabla de verdad** (truth table) | Every interpretation, with the relevant rows highlighted. The *subfórmulas* box adds a column for each subformula |
| **Forma clausal** (clausal form) | The five steps to reach the conjunctive normal form of each formula |
| **Resolución** (resolution) | The derivation of the empty clause, numbered and with every step justified |

* 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*.

<Tip>
  The formulas are stored in the page address: copy the link to share a specific exercise.
</Tip>

## 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**:

| Connective | Symbol | Also read as |
| - | - | - |
| Negation | $\lnot p$ | not $p$; it is false that $p$ |
| Conjunction | $p \land q$ | $p$ and $q$; $p$ **but** $q$; $p$ however $q$ |
| Disjunction | $p \lor q$ | $p$ or $q$ (or both) |
| Conditional | $p \to q$ | if $p$ then $q$; $p$ **only if** $q$; $q$ **is necessary** for $p$; $p$ **is sufficient** for $q$; not $p$ **unless** $q$ |
| Biconditional | $p \leftrightarrow q$ | $p$ if and only if $q$ |

<Warning>
  "$p$ only if $q$" is $p \to q$, not $q \to p$: "someone is Spanish only if they are European" says that being Spanish forces being European, not the other way round. What is **necessary** goes to the right of the arrow and what is **sufficient**, to the left.
</Warning>

### 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:

| $G$ | $H$ | $\lnot G$ | $G \land H$ | $G \lor H$ | $G \to H$ | $G \leftrightarrow H$ |
| - | - | - | - | - | - | - |
| V | V | F | V | V | V | V |
| V | F | F | F | V | **F** | F |
| F | V | V | F | V | V | F |
| F | F | V | F | F | V | V |

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

| Type | Definition |
| - | - |
| **Valid** (tautology) | True under every interpretation |
| **Satisfiable** | True under some interpretation |
| **Unsatisfiable** (contradiction) | False under every interpretation |

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:

| Law | Equivalence |
| - | - |
| Conditional elimination | $G \to H \equiv \lnot G \lor H$ |
| Contraposition | $G \to H \equiv \lnot H \to \lnot G$ |
| Biconditional elimination | $G \leftrightarrow H \equiv (G \to H) \land (H \to G)$ |
| Double negation | $\lnot\lnot G \equiv G$ |
| De Morgan | $\lnot(G \land H) \equiv \lnot G \lor \lnot H \qquad \lnot(G \lor H) \equiv \lnot G \land \lnot H$ |
| Distributive | $G \lor (H \land J) \equiv (G \lor H) \land (G \lor J)$ |
| Absorption | $G \land (H \lor G) \equiv G \qquad G \lor (H \land G) \equiv G$ |

### 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:

<Steps>
  <Step title="Eliminate ↔">
    $F \leftrightarrow G \equiv (F \to G) \land (G \to F)$
  </Step>

  <Step title="Eliminate →">
    $F \to G \equiv \lnot F \lor G$
  </Step>

  <Step title="Push negations inwards">
    With De Morgan's laws, until they only apply to propositions, removing double negations.
  </Step>

  <Step title="Distribute ∨ over ∧">
    $F \lor (G \land H) \equiv (F \lor G) \land (F \lor H)$
  </Step>

  <Step title="Simplify">
    Remove clauses that contain a literal and its complement (they are tautologies), repeated literals, and clauses absorbed by shorter ones.
  </Step>
</Steps>

### 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$.

<Tip>
  To check by resolution whether a single formula $F$ is valid, use the mirror principle: convert $\lnot F$ to clausal form and look for $\square$.
</Tip>

## Worked examples

<AccordionGroup>
  <Accordion title="Example 1 · The umbrella, with a truth table" defaultOpen>
    "If it is raining and there is no wind, I keep my umbrella open. My umbrella is not open, but it is raining. Therefore, it is windy."

    **Formalisation:** with $p$: it is raining, $q$: it is windy, and $r$: my umbrella is open,

    $\{p \land \lnot q \to r,\ \lnot r \land p\} \models q$

    **Table:** the second premise, $\lnot r \land p$, is only true when $p = V$ and $r = F$. That leaves two rows: with $q = V$, the first premise is $F \to F = V$; with $q = F$, it is $V \to F = F$. Both premises are true at the same time only in the row $p = V,\ q = V,\ r = F$, and there the conclusion $q$ is true.

    **Conclusion:** there is no counterexample. The argument is valid.
  </Accordion>

  <Accordion title="Example 2 · The umbrella, by resolution">
    **Clausal form of the premises:** $p \land \lnot q \to r \equiv \lnot(p \land \lnot q) \lor r \equiv \lnot p \lor q \lor r$. The second premise gives two clauses: $\lnot r$ and $p$.

    **Negated conclusion:** $\lnot q$.

    1. $\lnot p \lor q \lor r$ (premise 1)
    2. $\lnot r$ (premise 2)
    3. $p$ (premise 2)
    4. $\lnot q$ (negated conclusion)
    5. $\lnot p \lor q$, resolving 1 and 2 on $r$
    6. $q$, resolving 3 and 5 on $p$
    7. $\square$, resolving 4 and 6 on $q$

    The empty clause appears: the argument is valid.
  </Accordion>

  <Accordion title="Example 3 · Clausal form with a biconditional">
    Convert $\lnot(p \leftrightarrow \lnot q)$ to clausal form.

    **Eliminate ↔:** $\lnot\big((p \to \lnot q) \land (\lnot q \to p)\big)$

    **Eliminate →:** $\lnot\big((\lnot p \lor \lnot q) \land (\lnot\lnot q \lor p)\big)$

    **Push negations inwards:** $(p \land q) \lor (\lnot q \land \lnot p)$

    **Distribute:** $(p \lor \lnot q) \land (p \lor \lnot p) \land (q \lor \lnot q) \land (q \lor \lnot p)$

    **Simplify:** the clauses $p \lor \lnot p$ and $q \lor \lnot q$ are tautologies and disappear. Clausal form: $\{p \lor \lnot q,\ \lnot p \lor q\}$, which is exactly $p \leftrightarrow q$.
  </Accordion>

  <Accordion title="Example 4 · An invalid argument">
    "If I study, I pass. I passed. Therefore, I studied": $\{p \to q,\ q\} \models p$.

    In the row $p = F,\ q = V$ both premises are true ($F \to V = V$ and $q = V$) and the conclusion is false. That is a **counterexample**: the argument is not valid. It is the fallacy of affirming the consequent.

    By resolution: the clauses $\lnot p \lor q$, $q$ and $\lnot p$ have no complementary pair that gives anything new, so $\square$ never appears.
  </Accordion>

  <Accordion title="Example 5 · Classifying a formula">
    Is $\lnot p \lor q \land \lnot q \to \lnot p$ valid?

    With the precedence rules, it is $(\lnot p \lor (q \land \lnot q)) \to \lnot p$. Since $q \land \lnot q \equiv F$ and $\lnot p \lor F \equiv \lnot p$, the formula is equivalent to $\lnot p \to \lnot p$, which is always true. **It is valid.**

    On the other hand, $p \to q \lor r$ is satisfiable but not valid: it is false only when $p = V,\ q = F,\ r = F$.
  </Accordion>
</AccordionGroup>

## Try it in the simulator

<Steps>
  <Step title="Find the counterexample">
    Load "Falacia del consecuente" (affirming the consequent) and see which row turns red in the table. Change the second premise to $\lnot q$ and the conclusion to $\lnot p$ (that is *modus tollens*): does the counterexample disappear?
  </Step>

  <Step title="Three methods, one result">
    With lab example "Lab. 5b", compare the truth table (64 rows) with resolution. How many clauses does it take to reach $\square$?
  </Step>

  <Step title="The mirror principle">
    Type only $p \lor \lnot p$, with no conclusion. Then type $\lnot(p \lor \lnot p)$. What does the resolution tab show in each case?
  </Step>

  <Step title="Consistent or not">
    Enter $p \to q$, $p$ and $\lnot q$ as premises with no conclusion. Remove one of the three: which interpretation makes the other two true?
  </Step>

  <Step title="Precedence matters">
    Enter $p \to q \to r$ and $p \to (q \to r)$ as two separate formulas and turn on the subformulas in the table. Are they equivalent?
  </Step>
</Steps>

## 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

<AccordionGroup>
  <Accordion title="What is the difference between ⊨ and ⊢?">
    $\Gamma \models Q$ is logical consequence, defined with interpretations (semantics). $\Gamma \vdash Q$ means that $Q$ is **derived** from $\Gamma$ by applying inference rules (syntax). Resolution is sound and refutation-complete: $\Gamma \models Q$ if and only if $\square$ can be derived from $\Gamma \cup \{\lnot Q\}$.
  </Accordion>

  <Accordion title="Why does anything follow from inconsistent premises?">
    Because no interpretation makes them all true at once, so there can be no counterexample. By resolution, $\square$ already comes out of the premises without using the conclusion.
  </Accordion>

  <Accordion title="What is a Horn clause?">
    A clause with at most one positive literal, such as $\lnot p \lor \lnot q \lor r$, which is equivalent to $p \land q \to r$. They are Prolog's rules, and with them satisfiability can be decided in linear time.
  </Accordion>

  <Accordion title="Is this useful for simplifying conditions in a program?">
    Yes. With $p$ = `a < b` and $q$ = `c == d`, the condition `a < b || (a >= b && c == d)` is $p \lor (\lnot p \land q)$, which is equivalent to $p \lor q$. Type $p \lor (\lnot p \land q) \leftrightarrow p \lor q$ into the simulator and you will see it is valid.
  </Accordion>

  <Accordion title="How does it relate to Boolean algebra?">
    It is the same structure with a different notation: ∧ is the product, ∨ the sum and ¬ the complement (or the bar). A tautology in logic is, in electronics, a circuit whose output is always 1.
  </Accordion>
</AccordionGroup>

## Related simulators

These simulators and their notes are in Spanish.

<CardGroup cols={3}>
  <Card title="Truth table from an expression" icon="table" href="https://simulab.es/electronica/expresiones">
    The same idea in Boolean algebra notation, with the gate circuit.
  </Card>

  <Card title="Karnaugh maps" icon="table-cells" href="https://simulab.es/electronica/karnaugh">
    Simplifying logic functions of up to four variables.
  </Card>

  <Card title="Logic gates" icon="microchip" href="https://simulab.es/electronica/puertas-logicas">
    AND, OR, NOT, XOR and their truth tables.
  </Card>
</CardGroup>


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.