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 7Prof. 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 !