Logical proofs

Logical methods for AI

Logical proofs

Lecture 7

What you’ll be able to do

Checking reasoning

A proof: every step explicit.
A machine can search for a proof, or check one.
An AI proposes a proof; Lean checks it.

Step by step

Each conclusion can be used in a later step.

Proof systems

Axiomatic systems: axioms (glossary, opens in a new tab) , few rules.
Sequent calculi: judgments about assumptions and conclusions.
Tableaux, resolution: systematic search.
Natural deduction: rules for each connective.

Derivability

Natural deduction

$(RAIN \lor WIND) \to COLD$ , $COLD \to HEATING$ , $RAIN ⊢ HEATING$

Introduction and elimination

Discharge

$\to Intro$ : assume $A$ , derive $B$ , conclude $A \to B$ and discharge $[A]$ .

Temporary assumptions

$⊢ RAIN \to (RAIN \lor WIND)$

Reasoning by cases

$SUN \lor RAIN, \negSUN ⊢ RAIN$

Classical reasoning

$\neg⊥$ : a temporary assumption $\negA$ leads to $⊥$ , so $A$ . Without it: intuitionistic logic (glossary, opens in a new tab) .

Finding a derivation

A derivation exists; finding it is proof search (glossary, opens in a new tab) . Work backwards from the goal:

$A \land B$ : prove each conjunct, then $\land Intro$ .
$A \to B$ : assume $A$ , prove $B$ , then $\to Intro$ .
Stuck: assume the negation of the goal and derive $⊥$ .

Construct a derivation

Theorem provers

Proof assistants

A proof assistant (glossary, opens in a new tab) : we guide the construction; it checks every step. Lean, Rocq, Isabelle.

Automated provers

An automated theorem prover (glossary, opens in a new tab) searches for the proof itself: resolution, SAT solving. Vampire; SMT solvers such as Z3.

Types and type checking

$n : ℕ$ , and $n + 1 : ℕ$ .
$a : A$ : a proof term (glossary, opens in a new tab) of the proposition $A$ .

Proving $A$ : constructing a term of type $A$ . Checking the proof: checking its type.

The heating proof in Lean

Finding a proof in Lean

leanvariable (A B : Prop)

example : A → (B → (A ∧ B)) := by
  intro a
  intro b
  apply And.intro
  · sorry
  · sorry

$intro a$ : assume $a : A$ ; the goal becomes $B \to (A \land B)$ .
$apply And.intro$ : one goal per conjunct.
$sorry$ : a placeholder, not a proof. Here: $exact a$ , $exact b$ .

Curry–Howard

Propositions are types; proofs are programs: the Curry–Howard correspondence (glossary, opens in a new tab) .

Natural deduction	Lean command
$\land Intro$	$exact And.intro a b$
$\land Elim$	$exact And.left h$ , $exact And.right h$
$\lor Intro$	$exact Or.inl a$ , $exact Or.inr b$
$\lor Elim$	$apply Or.elim h$ , then prove both cases
$\to Intro$	$intro a$ , then prove $B$
$\to Elim$	$exact f a$

Logical proofs

Logical proofs

What you’ll be able to do

Checking reasoning

Step by step

Proof systems

Derivability

Natural deduction

Introduction and elimination

Discharge

Temporary assumptions

Reasoning by cases

Classical reasoning

Finding a derivation

Construct a derivation

Theorem provers

Proof assistants

Automated provers

Types and type checking

The heating proof in Lean

Finding a proof in Lean

Curry–Howard

Derivation and Lean