• English only

# Differences

This shows you the differences between two versions of the page.

 sav08:interpolants_from_resolution_proofs [2008/03/18 10:49]tatjana sav08:interpolants_from_resolution_proofs [2008/03/26 20:26] (current)piskac Both sides previous revision Previous revision 2008/03/26 20:26 piskac 2008/03/18 10:49 tatjana 2008/03/18 10:05 tatjana 2008/03/12 13:31 vkuncak 2008/03/12 13:31 vkuncak 2008/03/12 01:11 vkuncak 2008/03/12 01:10 vkuncak 2008/03/12 01:06 vkuncak 2008/03/12 01:06 vkuncak 2008/03/12 01:05 vkuncak 2008/03/11 16:45 vkuncak created 2008/03/26 20:26 piskac 2008/03/18 10:49 tatjana 2008/03/18 10:05 tatjana 2008/03/12 13:31 vkuncak 2008/03/12 13:31 vkuncak 2008/03/12 01:11 vkuncak 2008/03/12 01:10 vkuncak 2008/03/12 01:06 vkuncak 2008/03/12 01:06 vkuncak 2008/03/12 01:05 vkuncak 2008/03/11 16:45 vkuncak created Line 21: Line 21: * if $q \in FV(A) \setminus FV(B)$ then $I(C) = I(C_1) \lor I(C_2)$ * if $q \in FV(A) \setminus FV(B)$ then $I(C) = I(C_1) \lor I(C_2)$ * if $q \in FV(B) \setminus FV(A)$ then $I(C) = I(C_1) \land I(C_2)$ * if $q \in FV(B) \setminus FV(A)$ then $I(C) = I(C_1) \land I(C_2)$ - * if $q \in FV(A) \cap FV(B)$ then $I(C) = ite(q,I(C_2),I(C_1))$ + * if $q \in FV(A) \cap FV(B)$ then $I(C) = ite(q,I(C_1),I(C_2))$ We prove that $I(C)$ has the desired property by induction on the structure of the resolution proof tree. We prove that $I(C)$ has the desired property by induction on the structure of the resolution proof tree.

sav08/interpolants_from_resolution_proofs.txt · Last modified: 2008/03/26 20:26 by piskac

© EPFL 2018 - Legal notice