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 …