[Logiweb] Re: Quantifier elimination leads to variable clash

Ole Hyldahl Hansen hyldahl at diku.dk
Tue Jun 21 08:53:03 CEST 2005


On Mon, 20 Jun 2005, Anders B0ggild-Povlsen wrote:

> If I remenber correctly, Klaus suggested that you prove the lemma with any 
> free meta variables and use that lemma to prove the same thing using the meta 
> variables you wanted to use in the first place.
>
> In your case you could begin by proving (D=>E) => (D=>F=>E) and use that 
> lemma to prove (A => B) => (A => C => B). That should avoid variable clash.

You're right. That was indeed the suggestion. At least it should work for 
now. Thanks for reminding me.

Ole


More information about the Logiweb mailing list