Re: [isabelle] What auto actually can do



Which document exactly do you refer to?

In principle, you may think of 'auto' as a combination of 'blast' and 'simp' (please correct me, if I am telling nonsense). That means that some rules that are setup as 'natural deduction' rules as well as rewriting are used for proving goals.

1) Only because some tutorial states a proof in some detail, does not necessarily mean that it would not be provable using just an automatic method.

2) Even if there is a natural deduction proof for some goal, the automated methods might fail to produce it due to lack of time, misconfiguration, etc.

cheers

chris

On 03/23/2010 01:48 PM, Steve W wrote:
Hi all,

I have a quick question about what auto actually can do. On page 72 in the
tutorial, the proof for imp_uncurry seems to use only natural deduction. How
come the user needs to manually decide each step and not use auto for it?
What rules does auto actually have and what can/can't it do?

Thanks for the help.

Steve







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