Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] What auto actually can do


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC