Logic and Proof

Computer Science Tripos Part IB Michaelmas Term

Lawrence C Paulson Computer Laboratory University of Cambridge lp15@cam.ac.uk

Copyright c 2004 by Lawrence C. Paulson

Contents
1 Introduction 2 Propositional Logic 3 Gentzens Logical Calculi 4 Binary Decision Diagrams 5 First-Order Logic 6 Formal Reasoning in First-Order Logic 7 Davis-Putnam & Propositional Resolution 8 Skolem Functions and Herbrands Theorem 9 Unication 10 Resolution and Prolog 11 Modal Logics 12 Tableaux-Based Methods 1 6 11 16 21 26 32 38 43 49 54 59

Logic and Proof

Introduction to Logic

Logic concerns statements in some language. Slide 101 The language can be informal (say English) or formal. Some statements are true, others false or meaningless. Logic concerns relationships between statements: consistency, entailment, . . . Logical proofs model human reasoning (supposedly).

Statements
Statements are declarative assertions: Slide 102 Black is the colour of my true loves hair. They are not greetings, questions or commands: What is the colour of my true loves hair? I wish my true love had hair. Get a haircut!

Lawrence C. Paulson

University of Cambridge

Logic and Proof

Schematic Statements
The meta-variables Slide 103

X, Y , Z, . . . range over real objects

Black is the colour of Xs hair. Black is the colour of Y .

Z is the colour of Y .
Schematic statements can express general statements, or questions: What things are black?

Interpretations and Validity

An interpretation maps meta-variables to real objects: Slide 104 The interpretation Y

coal satises the statement

Black is the colour of Y . but the interpretation Y

strawberries does not!

A statement A is valid if all interpretations satisfy A.

Lawrence C. Paulson

University of Cambridge

Logic and Proof

Consistency, or Satisability
A set S of statements is consistent if some interpretation satises all elements of S at the same time. Otherwise S is inconsistent. Slide 105 Examples of inconsistent sets:

{X part of Y, Y part of Z, X NOT part of Z} {n is a positive integer, n = 1, n = 2, . . .}

Satisable means the same as consistent. Unsatisable means the same as inconsistent.

Entailment, or Logical Consequence

A set S of statements entails Slide 106

A if every interpretation that satises all elements of S, also satises A. We write S | A. = {X part of Y, Y part of Z} |= X part of Z {n = 1, n = 2, . . .} |= n is NOT a positive integer

S |= A if and only if {A} S is inconsistent |= A if and only if A is valid, if and only if {A} is inconsistent.

Lawrence C. Paulson

University of Cambridge

Logic and Proof

Inference
We want to check A is valid. Checking all interpretations can be effective but what if there are Slide 107 innitely many? Let {A1 , . . . , An }

|= B. If A1 , . . ., An are true then B must be A1 ... B An

true. Write this as the inference rule

We can use inference rules to construct nite proofs!

Schematic Inference Rules

X part of Y Y part of Z X part of Z

Slide 108 A valid inference:

spoke part of wheel wheel part of bike spoke part of bike

An inference may be valid even if the premises are false!

cow part of chair chair part of ant cow part of ant

Lawrence C. Paulson

University of Cambridge

Logic and Proof

Survey of Formal Logics

propositional logic is traditional boolean algebra. Slide 109 rst-order logic can say for all and there exists. higher-order logic reasons about sets and functions. modal/temporal logics reason about what must, or may, happen. type theories support constructive mathematics. All have been used to prove correctness of computer systems.

Why Should the Language be Formal?

Consider this denition: Slide 110 The least integer not denable using eight words Greater than The number of atoms in the entire Universe Also greater than The least integer not denable using eight words

A formal language prevents AMBIGUITY.

Lawrence C. Paulson

University of Cambridge

II

Logic and Proof

Syntax of Propositional Logic

P, Q, R, . . . t
Slide 201

propositional letter true false not A

f A AB AB AB AB

A and B A or B
if A then B

A if and only if B

Semantics of Propositional Logic

, , , and are truth-functional: functions of their operands.

Slide 202

A B t t f f t f t f

A f f t t

AB t f f f

AB t t t f

AB t f t t

AB t f f t

Lawrence C. Paulson

University of Cambridge

II

Logic and Proof

Interpretations of Propositional Logic

An interpretation is a function from the propositional letters to {t, f }. Slide 203 Interpretation I satises a formula A if the formula evaluates to t. Write | I =

A is valid (a tautology ) if every interpretation satises A. Write | A = S is satisable if some interpretation satises every formula in S.

Implication, Entailment, Equivalence

A B means simply A B.
Slide 204

A |= B means if |=I A then |=I B for every interpretation I. A |= B if and only if |= A B.

Equivalence

A A

B means A |= B and B |= A. B if and only if |= A B.

Lawrence C. Paulson

University of Cambridge

II

Logic and Proof

Equivalences

AA AB
Slide 205

A BA A (B C) (A B) (A C) f A f

(A B) C A (B C) Af At A A

Dual versions: exchange with and t with f in any equivalence

Negation Normal Form

1. Get rid of and , leaving just , , :

AB
Slide 206

(A B) (B A) A B

AB

2. Push negations in, using de Morgans laws:

A (A B) (A B)

A A B A B

Lawrence C. Paulson

University of Cambridge

II

Logic and Proof

From NNF to Conjunctive Normal Form

3. Push disjunctions in, using distributive laws:

A (B C)
Slide 207 4. Simplify:

(A B) (A C) (B A) (C A)

(B C) A

Delete any disjunction containing P and P Delete any disjunction that includes another: for example, in (P Q) P, delete P Q. Replace (P A) (P A) by A

Converting a Non-Tautology to CNF

PQQR
Slide 208 1. Elim : 2. Push in: 3. Push in: 4. Simplify: Not a tautology: try P

(P Q) (Q R) (P Q) (Q R) (P Q R) (Q Q R) P Q R t, Q f , R f

Lawrence C. Paulson

University of Cambridge

II

Logic and Proof

10

Tautology checking using CNF

((P Q) P) P
1. Elim : Slide 209 2. Push in:

[(P Q) P] P [(P Q) P] P [(P Q) P] P (P Q P) (P P) tt t

Its a tautology!

3. Push in: 4. Simplify:

Lawrence C. Paulson

University of Cambridge

III

Logic and Proof

11

A Simple Proof System

Axiom Schemes K Slide 301 S DN

A (B A) (A (B C)) ((A B) (A C)) A A

Inference Rule: Modus Ponens

AB B

A Simple (?) Proof of A

(A ((D A) A))
Slide 302

(1)

((A (D A)) (A A)) by S A ((D A) A) by K (A (D A)) (A A) by MP, (1), (2) A (D A) by K A A by MP, (3), (4)
(2) (3) (4) (5)

Lawrence C. Paulson

University of Cambridge

III

Logic and Proof

12

Some Facts about Deducibility

Slide 303

A is deducible from the set S if there is a nite proof of A starting from elements of S. Write S A.
Soundness Theorem. If S

A then S |= A. |= A then S B then S A. A B.

Completeness Theorem. If S

Deduction Theorem. If S {A}

Gentzens Natural Deduction Systems

The context of assumptions may vary. Each logical connective is dened independently. Slide 304 The introduction rule for shows how to deduce A B:

A B AB
The elimination rules for shows what to deduce from A B:

AB A

AB B

Lawrence C. Paulson

University of Cambridge

III

Logic and Proof

13

The Sequent Calculus

Sequent A1 , . . . , Am B1 , . . . , Bn means, Slide 305 if A1

. . . Am then B1 . . . Bn

A1 , . . ., Am are assumptions; B1 , . . ., Bn are goals and are sets in

The sequent A,

A, is trivially true (basic sequent).

Sequent Calculus Rules

, A A, (cut)
Slide 306

, A A, A, B, A B,

(l)

A, , A

(r)

(l)

, A , B , A B

(r)

Lawrence C. Paulson

University of Cambridge

III

Logic and Proof

14

More Sequent Calculus Rules

Slide 307

A, B, A B, , A B, A B,

(l)

, A, B , A B

(r)

(l)

A, , B , A B

(r)

Easy Sequent Calculus Proofs

Slide 308

A, B A (l) A BA (r) (A B) A A, B B, A (r) A B, B A (r) A B, B A (r) (A B) (B A)

Lawrence C. Paulson

University of Cambridge

III

Logic and Proof

15

Part of a Distributive Law

Slide 309

B, C A, B (l) A A, B B C A, B (l) A (B C) A, B (r) A (B C) A B similar A (B C) (A B) (A C)

(r)

Second subtree proves A (B C) A C similarly

A Failed Proof

Slide 310

A B, C B B, C (l) A B B, C (r) A BB C (r) (A B) (B C) A t, B f , C f falsies unproved sequent!

Lawrence C. Paulson

University of Cambridge

IV

Logic and Proof

16

BDDs: Binary Decision Diagrams

A canonical form for boolean expressions: decision trees with sharing.

ordered propositional symbols (variables)

Slide 401

sharing of identical subtrees hashing and other optimisations

Detects if a formula is tautologous (t) or inconsistent (f ). Exhibits models if the formula is satisable. Excellent for verifying digital circuits, with many other applications.

Decision Diagram for (P

Q) R

P
Slide 402

Q R 0 0 0 R 1 R 0 1

Q R 0 1

Lawrence C. Paulson

University of Cambridge

IV

Logic and Proof

17

Converting a Decision Diagram to a BDD

P Q R Q R Q

Slide 403

No duplicates

No redundant tests

Building BDDs Efciently

Do not construct full tree! Slide 404 Do not expand , , (exclusive OR) to other connectives. Treat Z as Z

f or Z t.

Recursively convert operands to BDDs. Combine operand BDDs, respecting the ordering and sharing. Delete redundant variable tests.

Lawrence C. Paulson

University of Cambridge

IV

Logic and Proof

18

Canonical Form Algorithm

To convert Z Z , where Z and Z are already BDDs: Slide 405 Let Z Trivial if either operand is t or f .

= if (P, X, Y) and Z = if (P , X , Y )

If P = P then recursively convert if (P, X X , Y Y ). If P < P then recursively convert if (P, X Z , Y Z ). If P > P then recursively convert if (P , Z X , Z Y ).

Canonical Forms of Other Connectives

Z Z , Z Z and Z Z are converted to BDDs similarly.

Slide 406 Some cases, like Z

t, reduce to negation.

Here is how to convert Z, where Z is a BDD:

If Z = if (P, X, Y) then recursively convert if (P, X, Y). if Z = t then return f , and if Z = f then return t.
In effect we copy the BDD but swap t and f at the leaves.

Lawrence C. Paulson

University of Cambridge

IV

Logic and Proof

19

Canonical Form (that is, BDD) of P

P
Slide 407

P 0 1

Q 1

Canonical Form of P

QQR

P Q
Slide 408

P Q R R 1 0 1 Q

P Q 0 1

Lawrence C. Paulson

University of Cambridge

IV

Logic and Proof

20

Optimisations Based On Hash Tables

Never build the same BDD twice, but share pointers. Advantages: Slide 409

If X Y , then the addresses of X and Y are equal. Can see if if (P, X, Y) is redundant by checking if X = Y . Can quickly simplify special cases like X X.
Never convert X Y twice, but keep a table of known canonical forms.

Final Observations
The variable ordering is crucial. Consider this formula:

(P1 Q1 ) (Pn Qn )
A good ordering is P1 Slide 410 linear. With P1

< Q1 < < Pn < Qn : the BDD is

< < Pn < Q1 < < Qn , the BDD is

EXPONENTIAL .

Many digital circuits have small BDDs: adders, but not multipliers. BDDs can solve problems in hundreds of variables. The general case remains hard (it is NP-complete).

Lawrence C. Paulson

University of Cambridge

Logic and Proof

21

Outline of First-Order Logic

Reasons about functions and relations over a set of individuals:

Slide 501

father(father(x)) = father(father(y)) cousin(x, y)

Reasons about all and some individuals: All men are mortal Socrates is a man Socrates is mortal Cannot reason about all functions or all relations, etc.

Function Symbols; Terms

Each function symbol stands for an n-place function. A constant symbol is a 0-place function symbol. Slide 502 A variable ranges over all individuals. A term is a variable, constant or a function application

f(t1 , . . . , tn )
where f is an n-place function symbol and t1 , . . ., tn are terms. We choose the language, adopting any desired function symbols.

Lawrence C. Paulson

University of Cambridge

Logic and Proof

22

Relation Symbols; Formulae

Each relation symbol stands for an n-place relation. Slide 503 Equality is the 2-place relation symbol = An atomic formula has the form R(t1 , . . . , tn ) where R is an

n-place relation symbol and t1 , . . ., tn are terms.

A formula is built up from atomic formul using , , , and so forth. Later, we can add quantiers.

The Power of Quantier-Free FOL

It is surprisingly expressive, if we include strong induction rules. It is easy to equivalence of mathematical functions: Slide 504

p(z, 0) = 1 p(z, n + 1) = p(z, n) z

q(z, 1) = z q(z, 2 n) = q(z z, n) q(z, 2 n + 1) = q(z z, n) z

The prover ACL2 uses this logic and has been used in major hardware proofs.

Lawrence C. Paulson

University of Cambridge

Logic and Proof

23

Universal and Existential Quantiers

x A for all x, the formula A holds x A there exists x such that A holds
Slide 505 Syntactic variations:

xyz A abbreviates x y z A z . A B is an alternative to z (A B)

The variable x is bound in x A; compare with

f(x)dx

The Expressiveness of Quantiers

All men are mortal:

x (man(x) mortal(x))
Slide 506 All mothers are female:

x female(mother(x))
There exists a unique x such that A, sometimes written !x A

x [A(x) y (A(y) y = x)]

Lawrence C. Paulson

University of Cambridge

Logic and Proof

24

How do we interpret mortal(Socrates)?

Take an interpretation I Slide 507

= (D, I) of our rst-order language.

D is a non-empty set, called the domain or universe. I maps symbols to real elements, functions and relations: c a constant symbol f an n-place function symbol P an n-place relation symbol I[c] D I[f] Dn D I[P] Dn

How do we interpret cousin(Charles, y)?

A valuation supplies the values of free variables. It is a function V Slide 508

: variables D.

IV [t] extends V to a term t by the obvious recursion: IV [x] = V(x) IV [c] = I[c] IV [f(t1 , . . . , tn )] = I[f](IV [t1 ], . . . , IV [tn ])
def def def

if x is a variable

Lawrence C. Paulson

University of Cambridge

Logic and Proof

25

The Meaning of Truth in FOL

For interpretation I and valuation V , dene | I,V by recursion. =

|=I,V P(t)
Slide 509

if IV [t]

I[P] holds A and |=I,V B A holds for some m D

|=I,V t = u |=I,V A B |=I,V x A

Finally, we dene

if IV [t] equals IV [u] if | I,V =

if | I,V{m/x} =

|=I A

if | I,V =

A holds for all V .

Formula A is satisable if | I =

A for some I .

Lawrence C. Paulson

University of Cambridge

VI

Logic and Proof

26

Free vs Bound Variables

All occurrences of x in x A and x A are bound An occurrence of x is free if it is not bound: Slide 601

y z R(y, z, f(y, x))

In this formula, y and z are bound while x is free. May rename bound variables:

w z R(w, z , f(w, x))

Substitution for Free Variables

A[t/x] means substitute t for x in A: (B C)[t/x] is B[t/x] C[t/x]

Slide 602

(x B)[t/x] is x B (y B)[t/x] is y B[t/x] (P(u))[t/x] is P(u[t/x])

With A[t/x], no variable of t may be bound in A!

(x = y)

(y (x = y)) [y/x]

IS NOT EQUIVALENT TO

y (y = y)

Lawrence C. Paulson

University of Cambridge

VI

Logic and Proof

27

Some Equivalences for Quantiers

(x A)
Slide 603

x A x A A[t/x] x (A B) x (A B).

x A (x A) (x B)
B UT WE DO NOT HAVE

(x A) (x B)

Dual versions: exchange with and with

Further Quantier Equivalences

These hold only if x is not free in B. Slide 604

(x A) B (x A) B (x A) B

x (A B) x (A B) x (A B)

These let us expand or contract a quantiers scope.

Lawrence C. Paulson

University of Cambridge

VI

Logic and Proof

28

Reasoning by Equivalences

x (x = a P(x))

x (x = a P(a)) x (x = a) P(a)

Slide 605

P(a) z (P(z) P(a) P(b)) z P(z) P(a) P(b) z P(z) P(a) P(b) P(a) P(b) t

Sequent Calculus Rules for

A[t/x], x A,
Slide 606

(l)

, A , x A

(r)

Rule (l) can create many instances of x A Rule (r) holds provided N OT allowed to prove

x is not free in the conclusion!

P(y) P(y) P(y) y P(y)

(r)

T HIS IS NONSENSE !

Lawrence C. Paulson

University of Cambridge

VI

Logic and Proof

29

A Simple Example of the Rules

Slide 607

P(f(y)) P(f(y)) x P(x) P(f(y)) x P(x) y P(f(y))

(l) (r)

A Not-So-Simple Example of the Rules

Slide 608

P Q(y), P P, Q(y) Q(y) (l) P, P Q(y) Q(y) (l) P, x (P Q(x)) Q(y) (r) P, x (P Q(x)) y Q(y) (r) x (P Q(x)) P y Q(y)
In (l), we must replace x by y.

Lawrence C. Paulson

University of Cambridge

VI

Logic and Proof

30

Sequent Calculus Rules for

A, x A,
Slide 609 Rule (l) holds provided

(l)

, A[t/x] , x A

(r)

x is not free in the conclusion!

Rule (r) can create many instances of x A For example, to prove this counter-intuitive formula:

z (P(z) P(a) P(b))

Part of the Distributive Law

Slide 610

P(x) P(x), Q(x) (r) P(x) P(x) Q(x) (r) P(x) y (P(y) Q(y)) similar (l) x P(x) y (P(y) Q(y)) x Q(x) y . . . x P(x) x Q(x) y (P(y) Q(y))

(l) (l)

Second subtree proves x Q(x) y (P(y) Q(y)) similarly In (r), we must replace y by x.

Lawrence C. Paulson

University of Cambridge

VI

Logic and Proof

31

A Failed Proof

Slide 611

P(x), Q(y) P(x) Q(x) (r) P(x), Q(y) z (P(z) Q(z)) (l) P(x), x Q(x) z (P(z) Q(z)) (l) x P(x), x Q(x) z (P(z) Q(z)) (l) x P(x) x Q(x) z (P(z) Q(z))
We cannot use (l) twice with the same variable This attempt renames the x in x Q(x), to get y Q(y)

Lawrence C. Paulson

University of Cambridge

VII

Logic and Proof

32

Clause Form
Clause: a disjunction of literals

K1 Km L1 Ln
Slide 701 Set notation: Kowalski notation:

{K1 , . . . , Km , L1 , . . . , Ln } K1 , , Km L1 , , Ln L1 , , Ln K1 , , Km

Empty clause: Empty clause is equivalent to f , meaning CONTRADICTION !

Outline of Clause Form Methods

To prove A, obtain a contradiction from A: 1. Translate A into CNF as A1 Slide 702

Am

2. This is the set of clauses A1 , . . ., Am 3. Transform the clause set, preserving consistency Deducing the empty clause refutes A. An empty clause set (all clauses deleted) means A is satisable. The basis for SAT SOLVERS and RESOLUTION PROVERS.

Lawrence C. Paulson

University of Cambridge

VII

Logic and Proof

33

The Davis-Putnam-Logeman-Loveland Method

1. Delete tautological clauses: 2. For each unit clause {L}, Slide 703

{P, P, . . .}

delete all clauses containing L delete L from all clauses

3. Delete all clauses containing pure literals 4. Perform a case split on some literal DPLL is a decision procedure: it nds a contradiction or a model.

Davis-Putnam on a Non-Tautology

Consider P

QQR {Q} {R} {Q} {R} initial clauses {R} unit Q {R} unit P (also pure)
unit R (also pure)

Clauses are {P, Q} Slide 704

{P, Q} {P}

Clauses satisable by P

t, Q f , R f

Lawrence C. Paulson

University of Cambridge

VII

Logic and Proof

34

Example of a Case Split on P

{Q, R} {R, P} {R, Q} {P, Q, R} {P, Q} {P, Q}

Slide 705

{Q, R}

{R, Q} {R}

{Q, R} {R} {R, Q}

{Q} if P is true
unit Q unit R

{Q, R} {Q}

{R}

{Q} {Q}

if P is false unit R unit Q

SAT solvers in the Real World

Progressed from joke to killer technology in 10 years. Princetons zChaff has solved problems with more than one
Slide 706 million variables and 10 million clauses.

Applications include nding bugs in device drivers (Microsofts

SLAM project).

Typical approach: approximate the problem with a nite model;

encode it using Boolean logic; supply to a SAT solver.

Lawrence C. Paulson

University of Cambridge

VII

Logic and Proof

35

The Resolution Rule

From B A and B C infer A C In set notation, Slide 707

{B, A1 , . . . , Am } {B, C1 , . . . , Cn } {A1 , . . . , Am , C1 , . . . , Cn }

Some special cases:

{B}

{B, C1 , . . . , Cn } {C1 , . . . , Cn }

{B}

{B}

Simple Example: Proving P

Hint: use (A

QQP

B)

A B [P Q Q P] (P Q) (Q P) (P Q) (Q P)

1. Negate! Slide 708 2. Push in:

Clauses:

{P}

{Q}

{Q, P}

Resolve {P} and {Q, P} getting {Q}. Resolve {Q} and {Q} getting : we have refuted the negation.

Lawrence C. Paulson

University of Cambridge

VII

Logic and Proof

36

Another Example
Refute [(P From (P Slide 709

Q) (P R) P (Q R)]

Q) (P R), get clauses {P, Q} and {P, R}. (Q R)] get clauses {P} and {Q, R}.

From [P

Resolve {P} and {P, Q} getting {Q}. Resolve {P} and {P, R} getting {R}. Resolve {Q} and {Q, R} getting {R}. Resolve {R} and {R} getting , contradiction.

The Saturation Algorithm

At start, all clauses are passive. None are active. Slide 710 1. Transfer a clause (current) from passive to active. 2. Form all resolvents between current and an active clause. 3. Use new clauses to simplify both passive and active. 4. Put the new clauses into passive. Repeat until CONTRADICTION found or passive becomes empty.

Lawrence C. Paulson

University of Cambridge

VII

Logic and Proof

37

Renements of Resolution
Subsumption: Slide 711 Preprocessing: Indexing: deleting redundant clauses removing tautologies, symmetries . . . elaborate data structures for speed

Ordered resolution: restrictions to focus the search Weighting: Set of Support: giving priority to the smallest clauses working on the goal, not the axioms

Lawrence C. Paulson

University of Cambridge

VIII

Logic and Proof

38

Reducing FOL to Propositional Logic

Prenex: Slide 801 Skolemize:

Move quantiers to the front Remove quantiers, preserving consistency

Herbrand models: Reduce the class of interpretations Herbrands Thm: Contradictions have nite, ground proofs Unication: Automatically nd the right instantiations

Finally, combine unication with resolution

Prenex Normal Form

Convert to Negation Normal Form using additionally

(x A)
Slide 802

x A x A

(x A)

Move quantiers to the front using (provided x is not free in B)

(x A) B (x A) B
and the similar rules for

x (A B) x (A B)

Lawrence C. Paulson

University of Cambridge

VIII

Logic and Proof

39

Skolemization, or Getting Rid of

(Can have k

Start with a formula of the form

= 0).

x1 x2 xk y A
Slide 803 Choose a fresh k-place function symbol, say f Delete y and replace y by f(x1 , x2 , . . . , xk ). We get

x1 x2 xk A[f(x1 , x2 , . . . , xk )/y]
Repeat until no quantiers remain

Example of Conversion to Clauses

For proving x [P(x)

y P(y)]

Slide 804

[x [P(x) y P(y)]] negated goal x [P(x) y P(y)] x y [P(x) P(y)] x [P(x) P(f(x))] {P(x)} {P(f(x))}
conversion to NNF pulling out Skolem term f(x) Final clauses

Lawrence C. Paulson

University of Cambridge

VIII

Logic and Proof

40

Correctness of Skolemization
The formula x y A is consistent

it holds in some interpretation I = (D, I)

Slide 805

for all x D there is some y D such that A holds ^ some function f in D D yields suitable values of y ^ A[f(x)/y] holds in some I extending I so that f denotes f the formula x A[f(x)/y] is consistent.
Dont panic if you cant follow this reasoning!

The Herbrand Universe for a set of clauses S

H0 = the set of constants in S (must be non-empty)

Slide 806

def

Hi+1 = Hi {f(t1 , . . . , tn ) | t1 , . . . , tn Hi
and f is an n-place function symbol in S}

def

H =

def i0

Hi

Herbrand Universe

H contains the terms expressible using the function symbols of S. Hi contains just the terms with at most i nested function applications.

Lawrence C. Paulson

University of Cambridge

VIII

Logic and Proof

41

Herbrand Interpretations for a set of clauses S

HB = {P(t1 , . . . , tn ) | t1 , . . . , tn H
and P is an n-place predicate symbol in S} Slide 807

def

HB contains all applications of predicates to elements of H.

Each subset of HB denes the cases where the predicates are true. A Herbrand model will interpret the predicates by some subset of HB. It will interpret function symbols by term-forming operations:

f denotes the function that puts f in front of the given arguments.

Example of an Herbrand Model

even(1) even(2)
Slide 808

clauses

even(X Y) even(X), even(Y)

H = {1, 2, 1 1, 1 2, 2 1, 2 2, 1 (1 1), . . .} HB = {even(1), even(2), even(1 1), even(1 2), . . .} I[even] = {even(2), even(1 2), even(2 1), even(2 2), . . .}
(for model where means product; could instead use sum!)

Lawrence C. Paulson

University of Cambridge

VIII

Logic and Proof

42

A Key Fact about Herbrand Interpretations

Let S be a set of clauses. Slide 809

S is unsatisable no Herbrand interpretation satises S Holds because some Herbrand model mimicks every real model We must consider only a small class of models Herbrand models are syntactic, easily processed by computer

Herbrands Theorem
Let S be a set of clauses.

S is unsatisable there is a nite unsatisable set S of ground instances of clauses of S.

Slide 810

Finite: we can compute it Instance: result of substituting for variables Ground: no variables remainits propositional!
Example:

S could be {P(x)} {P(f(y))}, and S could be {P(f(a))} {P(f(a))}.

Lawrence C. Paulson

University of Cambridge

IX

Logic and Proof

43

Unication
Finding a common instance of two terms. Lots of applications:

Prolog and other logic programming languages

Slide 901

Theorem proving: resolution and other procedures Tools for reasoning with equations Tools for satisfying multiple constraints Polymorphic type-checking (ML and other functional languages)
Its an intuitive generalization of pattern-matching.

Substitutions: A Mathematical Treatment

A substitution is a nite set of replacements

= [t1 /x1 , . . . , tk /xk ]

Slide 902 where x1 , . . ., xk are distinct variables and ti

= xi .

f(t, u) = f(t, u) P(t, u) = P(t, u) {L1 , . . . , Lm } = {L1 , . . . , Lm }

(substitution in terms) (in literals) (in clauses)

Lawrence C. Paulson

University of Cambridge

IX

Logic and Proof

44

Composing Substitutions
Composition of and , written , satises for all terms t

t( ) = (t)
Slide 903 It is dened by (for all relevant x)

= [ (x) / x, . . . ]
Consequences include []

def

= , and associativity :

( ) = ( )

Most General Uniers

is a unier of terms t and u if t = u. is more general than if = for some substitution .

Slide 904

is most general if it is more general than every other unier.

If unies t and u then so does :

t( ) = t = u = u( )
A most general unier of f(a, x) and f(y, g(z)) is [a/y, g(z)/x]. The common instance is f(a, g(z)).

Lawrence C. Paulson

University of Cambridge

IX

Logic and Proof

45

The Unication Algorithm

Represent terms by binary trees. Each term is a Variable x, y . . ., Constant Slide 905 S KETCH OF THE A LGORITHM . Constants do not unify with different Constants. Constants do not unify with Pairs. Variable x and term t: unier is [t/x], unless x occurs in t Cannot unify f(x) with x!

a, b . . ., or Pair (t, t )

The Unication Algorithm: The Case of Two Pairs

unies (t, t ) with (u, u )

Slide 906 if unies t with u and

unies t with u .

We unify the left sides, then the right sides. In an implementation, substitutions are formed by updating pointers. Composition happens automatically as more pointers are updated.

Lawrence C. Paulson

University of Cambridge

IX

Logic and Proof

46

Mathematical justication
Its easy to check that unies (t, t

) with (u, u ):

(t, t )( ) = (t, t )
Slide 907

= (t , t ) = (u , u ) = (u, u ) = (u, u )( ) is even a most general unier, if and are!

Four Unication Examples

f(x, b)
Slide 908

f(x, x) f(a, b)
None Fail

f(x, x) f(y, g(y))

None Fail

j(x, x, z) j(w, a, h(w)) j(a, a, h(a)) [a/w, a/x, h(a)/z]

f(a, y) f(a, b) [a/x, b/y]

Remember, the output is a substitution. The algorithm yields a most general unier.

Lawrence C. Paulson

University of Cambridge

IX

Logic and Proof

47

Theorem-Proving Example 1

(y x R(x, y)) (x y R(x, y))

Slide 909 After negation, the clauses are {R(x, a)} and {R(b, y)}. The literals R(x, a) and R(b, y) have unier [b/x, a/y]. We have the contradiction R(b, a) and R(b, s). T HE THEOREM IS PROVED BY CONTRADICTION !

Theorem-Proving Example 2

(x y R(x, y)) (y x R(x, y))

Slide 910 After negation, the clauses are {R(x, f(x))} and {R(g(y), y)}. The literals R(x, f(x)) and R(g(y), y) are not uniable. (They fail the occurs check.) We cant get a contradiction. F ORMULA IS NOT A THEOREM !

Lawrence C. Paulson

University of Cambridge

IX

Logic and Proof

48

Variations on Unication
Efcient unication algorithms: near-linear time Indexing & Discrimination networks: fast retrieval of a uniable term Slide 911 Associative/commutative unication

Example: unify a + (y + c) with (c + x) + b, get [a/x, b/y] Algorithm is very complicated The number of uniers can be exponential
Unication in many other theories (often undecidable!)

Lawrence C. Paulson

University of Cambridge

Logic and Proof

49

The Binary Resolution Rule

{B, A1 , . . . , Am } {D, C1 , . . . , Cn } {A1 , . . . , Am , C1 , . . . , Cn }

Slide 1001

provided B

= D

First, rename variables apart in the clauses! For example, given

{P(x)} and {P(g(x))}

rename x in one of the clauses before attempting unication. Always use a most general unier (MGU).

The Factoring Rule

This inference collapses uniable literals in one clause:

Slide 1002

{B1 , . . . , Bk , A1 , . . . , Am } {B1 , A1 , . . . , Am }
Example: Prove x y (P(y, x) The clauses are Factoring yields

provided B1

= = Bk

P(y, y)) {P(y, y), P(y, a)} {P(a, a)}

{P(y, a), P(y, y)} {P(a, a)}

Resolution yields the empty clause!

Lawrence C. Paulson

University of Cambridge

Logic and Proof

50

A Non-Trivial Proof

x [P Q(x)] x [Q(x) P] x [P Q(x)]

Clauses are {P, Q(b)} Slide 1003

{P, Q(x)} {P, Q(x)} {P, Q(a)}

getting {P, P} getting {P}

Resolve {P, Q(b)} with {P, Q(x)} Factor

{P, P} {P, P}

Resolve {P, Q(x)} with {P, Q(a)} getting {P, P} Factor getting {P} getting

Resolve {P} with {P}

What About Equality?

In theory, its enough to add the equality axioms:

The reexive, symmetric and transitive laws.

Slide 1004

Substitution laws like {x = y, f(x) = f(y)} for each f. Substitution laws like {x = y, P(x), P(y)} for each P.
In practice, we need something special: the paramodulation rule

{B[t ], A1 , . . . , Am } {t = u, C1 , . . . , Cn } {B[u], A1 , . . . , Am , C1 , . . . , Cn }

(if t

= t )

Lawrence C. Paulson

University of Cambridge

Logic and Proof

51

Prolog Clauses

Prolog clauses have a restricted form, with at most one positive literal. The denite clauses form the program. Procedure B with body Slide 1005 commands A1 , . . . , Am is

B A1 , . . . , Am
The single goal clause is like the execution stack, with say m tasks left to be done.

A1 , . . . , Am

Prolog Execution

Linear resolution:

Always resolve some program clause with the goal clause.

Slide 1006

The result becomes the new goal clause.

Try the program clauses in left-to-right order. Solve the goal clauses literals in left-to-right order. Use depth-rst search. (Performs backtracking, using little space.) Do unication without occurs check. (U NSOUND, but needed for speed)

Lawrence C. Paulson

University of Cambridge

Logic and Proof

52

A (Pure) Prolog Program

parent(elizabeth,charles). parent(elizabeth,andrew).

Slide 1007

parent(charles,william). parent(charles,henry). parent(andrew,beatrice). parent(andrew,eugenia). grand(X,Z) :- parent(X,Y), parent(Y,Z). cousin(X,Y) :- grand(Z,X), grand(Z,Y).

Prolog Execution
:- cousin(X,Y). :- grand(Z1,X), grand(Z1,Y). :- parent(Z1,Y2), parent(Y2,X), grand(Z1,Y). * :- parent(charles,X), grand(elizabeth,Y). X=william :- grand(elizabeth,Y). :- parent(elizabeth,Y5), parent(Y5,Y). * :- parent(andrew,Y). Y=beatrice :- .

Slide 1008

* = backtracking choice point

16 solutions including cousin(william,william) and cousin(william,henry)

Lawrence C. Paulson

University of Cambridge

Logic and Proof

53

Another FOL Proof Procedure: Model Elimination

A Prolog-like method to run on fast Prolog architectures. Contrapositives: treat clause {A1 , . . . , Am } like the m clauses Slide 1009

A1 A2 , . . . , Am A2 A3 , . . . , Am , A1
. . .

Am A1 , . . . , Am1
Extension rule: when proving goal P , assume P .

A Survey of Automatic Theorem Provers

Saturation (that is, resolution): E, Gandalf, SPASS, Vampire, . . . Slide 1010 Higher-Order Logic: TPS, LEO Model Elimination: Prolog Technology Theorem Prover, SETHEO Parallel ME: PARTHENON, PARTHEO Tableau (sequent) based: LeanTAP, 3TAP, . . .

Lawrence C. Paulson

University of Cambridge

XI

Logic and Proof

54

Modal Operators

W : set of possible worlds (machine states, future times, . . .) R: accessibility relation between worlds
Slide 1101

(W, R) is called a modal frame

2A means A is necessarily true 3A means A is possibly true 3A 2A

in all accessible worlds

A cannot be true A must be false

Semantics of Propositional Modal Logic

For a particular frame (W, R) An interpretation I maps the propositional letters to subsets of W Slide 1102

A means A is true in world w w w w w P 2A 3A w I(P) A and w B v v A for all v such that R(w, v) A for some v such that R(w, v)

A B w

Lawrence C. Paulson

University of Cambridge

XI

Logic and Proof

55

Truth and Validity in Modal Logic

For a particular frame (W, R), and interpretation I

w
Slide 1103

means A is true in world w means w means w

|=W,R,I A |=W,R A

A for all w in W A for all w and all I

|= A means |=W,R A for all frames; A is universally valid . . . but typically we constrain R to be, say, transitive
All tautologies are universally valid

A Hilbert-Style Proof System for K

Extend your favourite propositional proof system with Dist Slide 1104

2(A B) (2A 2B)

Inference Rule: Necessitation

A 2A
Treat 3 as a denition

3A = 2A

def

Lawrence C. Paulson

University of Cambridge

XI

Logic and Proof

56

Variant Modal Logics

Start with pure modal logic, which is called K Add axioms to constrain the accessibility relation: Slide 1105 T 4 B

2A A 2A 22A A 23A

(reexive) (transitive) (symmetric)

logic T logic S4 logic S5

And countless others! We shall mainly look at S4

Extra Sequent Calculus Rules for S4

A, 2A,
Slide 1106

(2l)

, A , 2A , A , 3A

(2r)

A, 3A,
def

(3l)

(3r)

= {2B | 2B } = {3B | 3B }
def

Erase non-2 assumptions Erase non-3 goals!

Lawrence C. Paulson

University of Cambridge

XI

Logic and Proof

57

A Proof of the Distribution Axiom

Slide 1107

A B, A B, A B A B, A B A B, 2A B 2(A B), 2A B 2(A B), 2A 2B

And thus 2(A

(l) (2l) (2l) (2r)

B) (2A 2B)

Must apply (2r) rst!

Part of an Operator String Equivalence

Slide 1108

3A 3A 23A 3A 323A 3A 2323A 3A 2323A 23A

In fact, 2323A

(2l) (3l) (2l) (2r)

23A

also 22A

2A

The S4 operator strings are

2 3 23 32 232 323

Lawrence C. Paulson

University of Cambridge

XI

Logic and Proof

58

Two Failed Proofs

Slide 1109

A 3A A 23A

(3r) (2r)

BA B B 3(A B) 3A, 3B 3(A B)

(3r) (3l)

Can extract a countermodel from the proof attempt

Lawrence C. Paulson

University of Cambridge

XII

Logic and Proof

59

Simplifying the Sequent Calculus

7 connectives (or 9 for modal logic):

Slide 1201

(2 3)

Left and right: so 14 rules (or 18) plus basic sequent, cut

Idea! Work in Negation Normal Form Fewer connectives:

(2 3)

Sequents need one side only!

Simplied Calculus: Left-Only

A, A,
Slide 1202

(basic)

A, A, (cut) A, B, A B, A, x A,

A, B, A B, A[t/x], x A,
Rule (l) holds provided

(l)

(l)

(l)

(l)

x is not free in the conclusion!

Lawrence C. Paulson

University of Cambridge

XII

Logic and Proof

60

Left-Only Sequent Rules for S4

A, 2A,
Slide 1203
def

(2l)

A, 3A,

(3l)

= {2B | 2B }
From 14 (or 18) rules to 4 (or 6)

Erase non-2 assumptions

Left-side only system uses proof by contradiction Right-side only system is an exact dual

Proving x (P

Q(x)) P y Q(y)

Move the right-side formula to the left and convert to NNF:

P y Q(y), x (P Q(x))
Slide 1204

P, Q(y), P P, Q(y), Q(y) (l) P, Q(y), P Q(y) (l) P, Q(y), x (P Q(x)) (l) P, y Q(y), x (P Q(x)) (l) P y Q(y), x (P Q(x))

Lawrence C. Paulson

University of Cambridge

XII

Logic and Proof

61

Adding Unication

Rule (l) now inserts a new free variable:

Slide 1205

A[z/x], x A,

(l)

Let unication instantiate any free variable In A, B,

try unifying A with B to make a basic sequent

Updating a variable affects entire proof tree What about rule (l)? Skolemize!

Skolemization from NNF

Dont pull quantiers out! Skolemize

[y z Q(y, z)] x P(x) to [y Q(y, f(y))] P(a)

Slide 1206 Its better to push quantiers in (called miniscoping) Example: proving x y [P(x) Negate; convert to NNF : Push in the y : Push in the x : Skolemize:

P(y)]:

x y [P(x) P(y)] x [P(x) y P(y)] (x P(x)) (y P(y)) x P(x) P(a)

Lawrence C. Paulson

University of Cambridge

XII

Logic and Proof

62

A Proof of x y [P(x)

P(y)]

Slide 1207

y f(z) (basic) P(y), P(f(y)), P(z), P(f(z)) (l) P(y), P(f(y)), P(z) P(f(z)) (l) P(y), P(f(y)), x [P(x) P(f(x))] (l) P(y) P(f(y)), x [P(x) P(f(x))] (l) x [P(x) P(f(x))]
Unication chooses the term for (l)

A Failed Proof
Try to prove x [P(x) Q(x)] x P(x) x Q(x) NNF : x P(x) x Q(x), Skolemize: Slide 1208

x [P(x) Q(x)]

P(a) Q(b), x [P(x) Q(x)]

ya y b??? P(a), Q(b), P(y) P(a), Q(b), Q(y) P(a), Q(b), P(y) Q(y) (l) P(a), Q(b), x [P(x) Q(x)] (l) P(a) Q(b), x [P(x) Q(x)]

(l)

Lawrence C. Paulson

University of Cambridge

XII

Logic and Proof

63

The Worlds Smallest Theorem Prover?

prove((A,B),UnExp,Lits,FreeV,VarLim) :- !, and prove(A,[B|UnExp],Lits,FreeV,VarLim). prove((A;B),UnExp,Lits,FreeV,VarLim) :- !, or prove(A,UnExp,Lits,FreeV,VarLim), prove(B,UnExp,Lits,FreeV,VarLim). prove(all(X,Fml),UnExp,Lits,FreeV,VarLim) :- !, forall \+ length(FreeV,VarLim), copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)), append(UnExp,[all(X,Fml)],UnExp1), prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim). prove(Lit,_,[L|Lits],_,_) :literals; negation (Lit = -Neg; -Lit = Neg) -> (unify(Neg,L); prove(Lit,[],Lits,_,_)). prove(Lit,[Next|UnExp],Lits,FreeV,VarLim) :next formula prove(Next,UnExp,[Lit|Lits],FreeV,VarLim).

Slide 1209

Lawrence C. Paulson

University of Cambridge