Theorem Proving for FOL Satisfiability Procedures CS294-8 Lecture 11 Prof.Necula CS 294-8 Lecture 11 1
Prof. Necula CS 294-8 Lecture 11 1 Theorem Proving for FOL Satisfiability Procedures CS 294-8 Lecture 11
Review Recall the we use the following logic: Goals: G::=LI true GiAG2 H>G VX.G Hypotheses: H :=L true HiA H2 Literals: L:=p(E1,....Ek) Expressions: E ::nI f(E1,...Em) This is sufficient for VCGen iff: The invariants,preconditions and postcond.are all from H Prof.Necula CS 294-8 Lecture 11 2
Prof. Necula CS 294-8 Lecture 11 2 Review • Recall the we use the following logic: Goals: G ::= L | true | G1 G2 | H G | x. G Hypotheses: H ::= L | true | H1 H2 Literals: L ::= p(E1 , …, Ek ) Expressions: E ::= n | f(E1 , …, Em) • This is sufficient for VCGen iff: – The invariants, preconditions and postcond. are all from H
A Simple and Complete Prover Define the following symbolic "prove"algorithm Prove(H,G)-prove the goal "H=G" Prove(H,true) true Prove(H,G1AG2)=prove(H,G1)&&prove(H,G2) Prove(H,Hi=G2)=prove(HA H1,G2) Prove(H,Vx.G) prove(H,G[a/x])(a is "fresh") Prove(H,L) unsat(HA-L) We have a simple,sound and complete prover If we have a way to check unsatisfiability of sets of literals Prof.Necula CS 294-8 Lecture 11 3
Prof. Necula CS 294-8 Lecture 11 3 A Simple and Complete Prover • Define the following symbolic “prove” algorithm – Prove(H, G) - prove the goal “H G” Prove(H, true) = true Prove(H, G1 G2 ) = prove(H, G1 ) && prove(H, G2 ) Prove(H, H1 G2 ) = prove(H H1 , G2 ) Prove(H, x. G) = prove(H, G[a/x]) (a is “fresh”) Prove(H, L) = unsat(H L) • We have a simple, sound and complete prover – If we have a way to check unsatisfiability of sets of literals
How Powerful is Our Prover? With VCGen in mind we must restrict invariants to H::=L true HiAH2 No disjunction,implication or quantification Is that bad Consider the function: void insert(LIST*a,LIST*b){ LIST*t=a->next;a->next=b;b->next=t; And the problem is to verify that It preserves linearity:all list cells are pointed to by at most one other list cell Provided that b is non-NULL and not pointed to by any cell Prof.Necula CS 294-8 Lecture 11 4
Prof. Necula CS 294-8 Lecture 11 4 How Powerful is Our Prover? • With VCGen in mind we must restrict invariants to H ::= L | true | H1 H2 • No disjunction, implication or quantification ! – Is that bad ? • Consider the function: void insert(LIST *a, LIST * b) { LIST *t = a->next; a->next = b; b->next = t; } • And the problem is to verify that – It preserves linearity: all list cells are pointed to by at most one other list cell – Provided that b is non-NULL and not pointed to by any cell
Lists and Linearity A bit of formal notation (remember the sel/upd): We write sel(n,a)to denote the value of "a->next"given the state of the "next"field is "n" We write upd(n,a,b)to denote the new state of the "next" field after "a->next b" Code is void insert(LIST*a,LIST*b){ LIST*t=a->next;a->next b;b->next =t; Pre is(付q.q≠0→p1.∀p2.sel(n,p1)=sel(n,p2)=q→p1=p2) Ab≠0∧p.sel(n,p)≠bAa≠0 Post is(q.q≠0→Vp1.∀p2.sel(n,p1)=sel(n,P2)=q→p1=p2) VC is Pre=Post[upd(upd(n,a,b),b,sel(n,a))/n]Not aG! Prof.Necula CS 294-8 Lecture 11 5
Prof. Necula CS 294-8 Lecture 11 5 Lists and Linearity • A bit of formal notation (remember the sel/upd): – We write sel(n, a) to denote the value of “a->next” given the state of the “next” field is “n” – We write upd(n, a, b) to denote the new state of the “next” field after “a->next = b” Code is void insert(LIST *a, LIST * b) { LIST *t = a->next; a->next = b; b->next = t; } Pre is (q.q 0 p1 .p2 .sel(n, p1 ) = sel(n, p2 ) = q p1 = p2 ) b 0 p.sel(n, p) b a 0 Post is (q. q 0 p1 .p2 . sel(n, p1 ) = sel(n, p2 ) = q p1 = p2 ) VC is Pre Post[upd(upd(n, a, b), b, sel(n, a)) / n] Not a G !
Two Solutions So it is quite easy to want to step outside H ·So what can we do? 1.Extend the language of H And then extend the prover 2.Push the complexity of invariants into literals And then extend the unsatisfiability procedure Prof.Necula CS 294-8 Lecture 11 6
Prof. Necula CS 294-8 Lecture 11 6 Two Solutions • So it is quite easy to want to step outside H • So what can we do? 1. Extend the language of H – And then extend the prover 2. Push the complexity of invariants into literals – And then extend the unsatisfiability procedure
Goal Directed Theorem Proving (1) Finally we extend the use of quantifiers: G:=L|true|G1∧62|H→G|x.G|3x.E H::=LI true HA H2 Yx.H We have now introduced an existential choice -Both in"H→3x.G"and"Vx.H→G” o Existential choices are postponed Introduce unification variables unification prove(H,3x.G)=prove(H,G[u/x])(u is a unif var) prove(H,u t)=instantiate u with t if u e FV(t) Still sound and complete goal directed proof search Provided that unsat can handle unification variables Prof.Necula CS 294-8 Lecture 11 7
Prof. Necula CS 294-8 Lecture 11 7 Goal Directed Theorem Proving (1) • Finally we extend the use of quantifiers: G ::= L | true | G1 G2 | H G | x. G | x. G H ::= L | true | H1 H2 | x. H • We have now introduced an existential choice – Both in “H x. G” and “x.H G” • Existential choices are postponed – Introduce unification variables + unification prove(H, x.G) = prove(H, G[u/x] ) (u is a unif var) prove(H, u = t) = instantiate u with t if u FV(t) • Still sound and complete goal directed proof search ! – Provided that unsat can handle unification variables !
Goal Directed Theorem Proving (2) We can add disjunction(but only to goals): G::trueLIGIAG2H>G VX.GI GYG2 Extend prover as follows: prove(H,G1VG2)=prove(H,Gi)I prove(H,G2) This introduces a choice point in proof search Called a "disjunctive choice" Backtracking is complete for this choice selection But only in intuitionistic logic! Prof.Necula CS 294-8 Lecture 11 8
Prof. Necula CS 294-8 Lecture 11 8 Goal Directed Theorem Proving (2) • We can add disjunction (but only to goals): G ::= true | L | G1 G2 | H G | x. G | G1 G2 • Extend prover as follows: prove(H, G1 G2 ) = prove(H, G1 ) || prove(H, G2 ) • This introduces a choice point in proof search – Called a “disjunctive choice” – Backtracking is complete for this choice selection • But only in intuitionistic logic !
Goal Directed Theorem Proving (3) Now we extend a bit the language of hypotheses Important since this adds flexibility for invariants and specs. H:=L|true|H1AH2|G→H We extend the prover as follows: prove(H,(G1→H)→G)= prove(H,G)(prove(HAH1,G)&&prove(H,Gi)) This adds another choice(clause choice in Prolog)expressed here also as a dis junctive choice Still complete with backtracking Prof.Necula CS 294-8 Lecture 11 9
Prof. Necula CS 294-8 Lecture 11 9 Goal Directed Theorem Proving (3) • Now we extend a bit the language of hypotheses – Important since this adds flexibility for invariants and specs. H ::= L | true | H1 H2 | G H • We extend the prover as follows: prove(H, (G1 H1 ) G) = prove(H, G) || (prove(H H1 , G) && prove(H, G1 )) – This adds another choice (clause choice in Prolog) expressed here also as a disjunctive choice – Still complete with backtracking
Goal Directed Theorem Proving (4) The VC for linear lists can be proved in this logic This logic is called Hereditary Harrop Formulas o But the prover is not complete in a classical sense And thus complications might arise with certain theories Still no way to have disjunctive hypotheses The prover becomes incomplete even in intuitionistic logic E.g.,cannot prove even that PvQQv P Let's try the other method instead .. Prof.Necula CS 294-8 Lecture 11 10
Prof. Necula CS 294-8 Lecture 11 10 Goal Directed Theorem Proving (4) • The VC for linear lists can be proved in this logic ! – This logic is called Hereditary Harrop Formulas • But the prover is not complete in a classical sense – And thus complications might arise with certain theories • Still no way to have disjunctive hypotheses – The prover becomes incomplete even in intuitionistic logic – E.g., cannot prove even that P Q Q P • Let’s try the other method instead …