Transcript TP1

Theorem proving
Alexander Serebrenik
1
TP for FM
• FM: proving properties of programs.
• Theorem proving: proving statements in
first-order logics (FOL).
• Hence:
statements
programs
and
properties
proof found
in FOL
Translator
Theorem
prover
no proof found
2
Today and Next Week
statements
programs
and
properties
proof found
in FOL
Translator
Theorem
prover
no proof found
in two weeks
3
Propositional Calculus – Reminder
• Predicates: p, q, r, …
• Connectors:
–  (“and”),
–  (“or”),
–  (“not”),
–  (“implies”)
• E.g. (p  q)  r
4
First Order Logics – reminder
•
•
•
•
Constants: ‘John Doe’, 1984, 3.14159…
Variables: x, y, z, …
Function symbols: f, g, h, …
Predicates: p, q, r, …
• Term: h(x), fatherOf(‘John Doe’)
• Atomic sentence:
married(fatherOf(‘John Doe’), ‘Jane Smith’)
5
Connectors and Quantifiers
•
•
Connectors: , , , 
married(x, ‘Jane’)  rich(x)
Quantifiers: , 
x (married(x, ‘Jane’)  rich(x))
• QQ: “Everybody needs somebody”
A. x y needs(x,y) C. x y needs(x,y)
B. x y needs(x,y) D. x y needs(x,y)
6
Variables: Free and Bound
• Intuition: variables that appear between ()
after ,  are called bound, otherwise they
are called free.
• QQ: Which variables are free in the
following sentence?
x ((p(x,y)  q(x))  z (r(v,z)  s(z)))
7
Questions so far?
• If these notions are not familiar…
• If you are not sure which variables are
free in x (p(x,y)  z q(z,x))…
• If you do not remember whether
(p(x)  q(y)) is equivalent to p(x)  q(y)
Check logics textbooks!
8
Some Sentences Are Always True
• If x and y are negative then x*y is positive.
• Any prime number greater than two is odd.
• We call this tautology and denote╞ φ
– φ - sentence
9
╞φ?
• Check whether for all variable
substitutions φ is evaluated to true.
10
Alternative
• We need a proof calculus
– number of syntactic inference rules
– when applied to axioms can produce φ
• Even better: reduce φ to axioms by
applying the rules!
• QQ: Why is the second option better?
11
Proofs
• If φ can be reduced to axioms by applying
the rules we write
├φ
• Proof = series of reduction steps
• φ is provable
12
Correctness Properties for ├
• Proof calculus should satisfy:
• Soundness: If├ φ then ╞ φ
– if something has been proved, it holds.
• Completeness: If ╞ φ then ├ φ
– if something holds, it can be proven.
13
System G
• a proof calculus for propositional calculus / firstorder logics
• sound and complete
• basis for automated theorem provers
We
• will see the axioms and the inference rules
• apply them to a number of examples
• discuss automation of the approach
14
System G is Based on:
Gentzen Sequent
ΓΔ
antecedents
succedents
finite sequences of logic sentences
15
Intuition
Let Γ be A1, …, An,
Δ be B1, …, Bm
Γ  Δ corresponds to
╞ ((A1  … An)  (B1  … Bm))
16
System G: Axioms
• Γ  Δ is an axiom if Γ Δ ≠ 
• QQ: Explain the choice of the axioms.
• Hint: recall the intuition behind Γ  Δ
17
System G: Inference Rules
• Depend on the outermost connector of quantifier.
• Conjunction (1):
, A, B,   
, A  B,   
 : left 
• A, B are arbitrary sentences
• Γ, Δ, Λ are sequences of sentences
• Read upwards:
– replace an antecedent A  B by two antecedents A
and B
18
System G: Try It Yourself!
• QQ: Prove (AB  A)
• Proof:
axiom since {A, B}  A
is not empty
A, B  A
apply  : left
A B  A
19
System G: :right
• What if we need to prove A  B?
• We need to prove two statements: A and B
 Replace one sequent by two:
  , A,    , B, 
  , A  B, 
 : right 
20
System G: Try It Yourself!
• QQ: Prove (A,B  AB)
• Proof:axioms since
the intersecti on
is not empty
A, B  A A, B  B
A, B  A  B
apply  : right
21
-symmetry (1)
, A, B,   
, A  B,   
  ,A, B, 
  , A  B, 
 : left 
 : right 
If we need to prove AB, we need to
prove at least one of A or B
22
-symmetry (2)
  , A,    , B, 
  , A  B, 
 : right 
, A,    , B,   
, A  B,   
 : left 
If we know AB, we either know A or we
know B.
23
Negation
,   A, 
, A,   
A,   , 
  , A, 
 : left 
 : right 
24
Implication: Try Yourself!
Group A
(: left )
?
, A  B ,   
Group B
(: right )
?
  , A  B, 
Reminder: AB is equivalent to AB.
  ,A, B, ( : right )
, A,    , B,   
( : left )
  ,A  B, 
, A  B,   
,   A, 
, A,   
( : left )
A,   ,  ( : right )
  , A, 
25
Implication: Group A
,   A, 
( : left )
, B ,   
, A,   
, A  B ,   
, A  B ,   
( : left )
Hence
,   A,  , B,   
, A  B ,   
: left 
26
Implication: Group B
A,   , B, 
  , A, B, 
   , A  B , 
  , A  B, 
( : right )
( : right )
Hence
A,   , B, 
  , A  B, 
: right 
27
… But How Can We Prove φ?
Start with φ
28
Example
• Prove A A:
A A
 A, A
A  A
 A  A
29
Summary So Far
• System G:
– based on the notion of a Gentzen sequent
– sequent: Γ  Δ
• Axioms: Γ  Δ is an axiom if Γ Δ ≠ 
• For propositional calculus:
8 inference rules ({,,,} * {left, right})
• For First-Order Logics: 4 more to come.
30
G for Propositional Calculus
• Sound and complete for propositional
calculus.
• There exists an algorithm that given a
sequent:
– always terminates
– proves the sequent if and only if it is a
tautology
– based on the notion of a proof tree, i.e., a tree
with nodes labelled by sequents
31
Algorithm (1)
algo search(ΓΔ)
T := one-node tree labeled with ΓΔ
while exists a leaf of T that can be expanded
CopyT := T
for each leaf node of CopyT
if the node is not an axiom
expand(node, T)
if all leaves are axioms
write(‘T is the proof of ΓΔ’)
else write(‘ΓΔ is not a tautology’)
32
Algorithm (2)
algo expand(node,T)
let node be labeled A1, … ,An  B1, … ,Bm
S := one-node tree labeled with A1, … ,An 
B1, … ,Bm
for i=1 to n
if nonatomic(Ai) then apply2all(Ai, left, S)
for i=1 to m
if nonatomic(Ai) then apply2all(Ai, right, S)
replace node in T by S
33
Algorithm: Let Us Try It!
search ( P  Q  Q  P)
exxpand( P  Q  Q  P, T)
S  one - node tree
apply 2all ( P  Q, left , S)
Tree T
P  Q  Q  P
Tree S
P  Q  Q  P
 P, Q  P Q  Q  P
apply 2all (Q  P, right , S)
Q , Q  P
Q  P, P
replace P  Q  Q  P in T by S
,
 A, ,B
,  , B,   
A
,
: right 

,,AA
B,B,   
: left 
34
Algorithm: Let Us Try It!
search ( P  Q  Q  P)
exxpand(Q
Q
, 
Q
P, P, T)
S  one - node tree
apply 2all (Q, left , S)
apply 2all (P, right , S)
Tree T
P  Q  Q  P
 P, Q  P Q  Q  P
Q  P, P
 Q , P , P
P  Q, P
replace Q  P, P in T by S
Q , Q  P
Tree S
Q  P, P
 Q , P , P
P  Q, P
35
Algorithm: Let Us Try It!
search ( P  Q  Q  P)
exxpand(Q  P, P, T)
Both leaves
are axioms!
Tree T
P  Q  Q  P
 P, Q  P Q  Q  P
Q  P, P
 Q , P , P
Q , Q  P
Q  P , Q
P  Q, P
Hence, T is the proof
of P  Q  Q  P
36
Algorithm: QQ
• To prove that our algorithm terminates we
have to find a certain value that decreases
from a parent node to each one of the
children nodes.
• What is this value?
37
Towards FOL: :left
• 
– if we know that x A(x) holds, then we can
chose any term t (not containing x) and
replace x by t.
– A[t/x] denotes replacement of all x’s in A by t
, A[t / x], xA,   
, xA,   
 : left 
QQ: Why do we keep x A?
38
Towards FOL: :right
• 
– if we need to prove that x A holds, we can
take any term t (not containing x) and replace
x A by A[t/x].
– if the proof of A[t/x] succeeds, then we have
also proved x A
– t is not necessarily unique, so we keep x A
  , A[t / x], xA, 
  , xA, 
 : right 
39
But what if we know x A?
• We still do not know for which x does A
hold! How can we guess?
• We do not need to guess! A new (unused)
variable: let y be such that A[y/x] holds!
, A[ y / x],   
, xA,   
 : left 
40
And If We Need to Prove x A?
• The same idea works!
• If A holds for a new unused variable y,
then it holds for any value
  , A[ y / x], 
  , xA, 
 : right 
41
QQ: Why Should y Be New?
• Otherwise, we loose soundness!
• Give an example.
42
Summary: System G for Quantifiers
, A[t / x], xA,   
, xA,   
, A[ y / x],   
, xA,   
 : left 
  , A[ y / x], 
  , xA, 
 : right 
 : left 
  , A[t / x], xA, 
  , xA, 
 : right 
43
QQ
, A[t / x], xA,   
, xA,   
 : left 
  , A[ y / x], 
  , xA, 
 : right 
Group A: Prove x A  A if A does not contain x.
Group B: Prove A  x A if A does not contain x.
44
System G for FOL
• Sound and complete
• There exists an algorithm that given a
sequent:
– proves the sequent if and only if it is a
tautology
– extends our previous algorithm
• However, termination is no longer
guaranteed
45
Hence
Algorithm
Terminates, the
proof has been
found.
Terminates, the
statement is not
a tautology
Does not
terminate
46
Even more bad news
• There exists no algorithm for FOL that
– always terminates, and
– proves the sequent if and only if it is a
tautology.
• In other words, the problem of deciding
whether an FOL formula is a tautology is
recursively enumerable, but not corecursively enumerable.
47
Reasons for Non-Termination (1)
, A[t / x], xA,   
 : left 
, xA,   
  , A[t / x], xA, 
  , xA, 
 : right 
• Repetitive application of (:left), (:right).
– it is useless to chose the same t twice for the
same A.
– for each term t keep a list of xA and xA
such that t has been used for the replacement
in (:left) or (:right).
48
Reasons for Non-Termination (2)
, A[t / x], xA,   
 : left 
, xA,   
  , A[t / x], xA, 
  , xA, 
 : right 
• As we have function symbols we have
infinitely many terms to choose from: {a,
f(a), f(f(a)), f(f(f(a))), …}
– either try all of them in some order
– or leave the choice to a human
49
How Shall We Adapt the Algorithm?
(1)
• List of variables {x0, x1, …, xn} appearing in
ΓΔ
• List of variables for (:right) and (:left):
{y1, y2, …}
– disjoint from {x0, x1, …, xn}
– a variable is removed from the list every time
these rules are applied
50
How Shall We Adapt the Algorithm?
(2)
• Structure TERM of pairs <t, S>
– S = a list of xA and xA such that t has been used
for the replacement in (:left) or (:right).
– initially: <c, nil>, where c is
• a constant or a free variable appearing in ΓΔ, if exists
• y0, otherwise
• List AVAIL of terms for (:left) and (:right):
– AVAIL0 - terms from free variables, constants (if exist)
or y0 (otherwise), and function symbols
– AVAILi - terms containing yi constructed from free
variables, constants, y1, …, yi, and function symbols
51
How Shall We Adapt the Algorithm?
(3)
• (:right) and (:left):
– Remove yi from {y1, y2, …}
– Add yi to TERM
– Remove yi from AVAILi
• (:left) and (:right):
  , A[ y / x], 
  , xA, 
, A[t / x], xA,   
, xA,   
– All terms from TERM are available
– Add first element from AVAILi to TERM and
remove it from AVAILi
52
Complete Algorithm?
• See handouts
53
We Have FOL, But We Need More
• We would like to compare terms, using =
, t  t  
(reflexivity )

for any f
, (s1  t1 )  ...  ( sn  t n )  ( f (s1 ,..., s n )  f (t1 ,..., t n ))  

for any P
, (( s1  t1 )  ...  (s n  t n )  P(s1 ,..., s n ))  P(t1 ,..., t n )  

54
System G=: QQ
axiom
x( x  f ( y)  P( x)), f ( y)  f ( y)  f ( y)  f ( y), P( f ( y))
reflexivity 
x( x  f ( y)  P( x))  f ( y)  f ( y), P( f ( y))
axiom
P( f ( y)), x( x  f ( y)  P( x))  P( f ( y))
: left 
f ( y)  f ( y)  P( f ( y)), x( x  f ( y)  P( x))  P( f ( y))
 : left 
substitution [ f ( y ) / x]
x( x  f ( y )  P( x))  P( f ( y ))
55
P Can Be =!
, (( s1  t1 )  ...  (s n  t n )  P(s1 ,..., s n ))  P(t1 ,..., t n )  

, (s1  t1 )  ( s 2  t 2 )  (s1  s 2 )  (t1  t 2 )  

56
Example: Symmetry of =
x  y  x  y, y  x T
y  x, x  y  y  x
x  y  x  y  x  x  x  x, y  x
x  y, ( x  y  x  x  x  x  y  x)  y  x
x y yx
T:
x  y, x  x  x  x, y  x x  y, x  x  x  x, y  x
x  y  x  x, y  x
x  y  x  x, y  x
x  y  x  x  x  x, y  x
57
Automation
• For propositional calculus – complete
– the user can make reasoning more efficient
• choice of A1, …, An  B1, …, Bm to apply an
inference rule.
• For FOL and FOL=
– only partial automation possible:
• choice of a term for the substitution.
• choice of A1, …, An  B1, …, Bm to apply an
inference rule.
58
Summary (1)
• Proving properties of programs is based on
proving logic formulae.
• To prove a formula one needs proof
calculus.
• Proof calculus should be sound and
complete.
• System G is based on the notion of a
sequent.
59
Summary (2)
• Sequent ΓΔ
– Γ, Δ are finite sequences of sentences
• System G for propositional calculus is sound
and complete.
– there is a proof algorithm that always terminates.
• System G for FOL is sound and complete.
– proof algorithm can go forever.
• System G= for FOL= is sound and complete.
– proof algorithm can go forever.
60
Next Lecture: PVS
• Prototype Verification System
– Developed at SRI International
– Open Source (GPL) since 1993
– Runs on Linux/Solaris/Mac
– Uses Emacs as Interface
– Supports System G reasoning…
– and much, much more!
• We will use it, so install it at your laptops!
61