Email Gateway (Aug 18 2022 at 14:57): Email Gateway (Aug 18 2022 at 14:57):From: Steve W <s.wong.731@googlemail.com>
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
Email Gateway (Aug 18 2022 at 14:57):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Email Gateway (Aug 18 2022 at 14:57):From: Tobias Nipkow <nipkow@in.tum.de>
Steve W wrote:
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
Last updated: Nov 21 2024 at 12:39 UTC