Re: [isabelle] What auto actually can do



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

The auto method is mostly rewriting with a bit of natural deduction
thrown in, but not much. The blast method is much superior if logic
without equational reasoning is concerned.

Tobias





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