Re: [isabelle] "apply auto" transforms provable statement to something false?



I havenât tried your particular example, but other examples are very easy to generate. Suppose you want to prove âx. x=0 & x=1.Then you can easily give yourself the two subgoals ?x=0 and ?x=1. Then auto will solve one and replace the other by False.

Larry Paulson


> On 25 Jan 2016, at 11:37, Eugene W. Stark <isabelle-users at starkeffect.com> wrote:
> 
> I wouldn't be surprised if the resulting subgoal was simply unprovable.
> What I am surprised about is the fact that it is false.  But I suppose
> that an incorrect instantiation of a schematic variable could produce
> this behavior.  In my limited mind's eye view of how theorem provers work,
> I was assuming that the instances would be generated by unification
> during resolution or something, which would not reduce true goals to
> false (not merely unprovable) subgoals.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.