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
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,
On 03/23/2010 01:48 PM, Steve W wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and