That's fine with me. I would not insist on breaking the current careful
separation of the constructive part of HOL.
Tobias
Lawrence Paulson schrieb:
> So, metis becomes available just before List.thy? This might be a good
> compromise.
> Larry
>
> On 14 Sep 2007, at 15:26, Florian Haftmann w
I'm a little surprised to hear Sledgehammer needs a general axiom of
choice. After all, first order logic doesn't. Could the uses of
Hilbert's choice in Sledgehammer be replaced with dynamic calls to
ax_specification? That gives you a lot of the power of Hilbert
choice, but is a conservativ
On Fri, 14 Sep 2007, Stefan Berghofer wrote:
> For those members of the list who have not followed the discussion
> about this issue a few years ago, let me cite what Larry wrote about it:
>
>I think it would be quite easy to do, and sensible (ZF has always been
> that way).
>
>[...]
>
So, metis becomes available just before List.thy? This might be a
good compromise.
Larry
On 14 Sep 2007, at 15:26, Florian Haftmann wrote:
> I would still argue that it is a good idea to have a non-Hilbertian
> entrance point to HOL (PreList); anyway there should be no problem to
> import Hilb
Lawrence Paulson wrote:
> We previously put some effort into making
> virtually all of HOL independent of the axiom of choice, so this
> would be a reversal. [...] Can anybody comment?
For those members of the list who have not followed the discussion
about this issue a few years ago, let me c
Why not ask the Isabelle community if such users are out there?
Clemens
On 14 Sep 2007, at 12:32, Lawrence Paulson wrote:
> However, I don't know of anybody who has
> actually taken advantage of the AC-free part;
Lawrence Paulson wrote:
> Metis also relies on clause form.
I would still argue that it is a good idea to have a non-Hilbertian
entrance point to HOL (PreList); anyway there should be no problem to
import Hilbert_Choice before List and then setup Metis and Sledgehammer.
Florian
-- ne
Lawrence Paulson wrote:
> It needs at least Hilbert_Choice. It could go before Datatype. Some
> details need to be worked out to ensure that all theorems in Main.thy
> get converted to clause form.
I must confess that I have lost track now. Does only the skolemization
depend on Hilbert-Choice, or
> Florian has suggested making sledgehammer available earlier in the
> construction of Main, before PreList at least. This could be useful
> to developers. However, it requires Hilbert_Choice, which must also
> be introduced earlier.
A PreList-Sledgehammer would be a nice thing to have, but
I would appreciate having at least metis early on. I have recently
wasted some time trying to figure out the details of a
sledgehammer/metis proof in order to add it to List.
Tobias
Lawrence Paulson schrieb:
> Florian has suggested making sledgehammer available earlier in the
> construction o
Metis also relies on clause form.
Larry
On 14 Sep 2007, at 15:21, Florian Haftmann wrote:
> I must confess that I have lost track now. Does only the
> skolemization
> depend on Hilbert-Choice, or also metis?
-- next part --
An HTML attachment was scrubbed...
URL:
http
It needs at least Hilbert_Choice. It could go before Datatype. Some
details need to be worked out to ensure that all theorems in Main.thy
get converted to clause form.
Larry
On 14 Sep 2007, at 14:46, Florian Haftmann wrote:
> A PreList-Sledgehammer would be a nice thing to have, but it is not
Lawrence Paulson writes:
> Florian has suggested making sledgehammer available earlier in the
> construction of Main, before PreList at least. This could be useful
> to developers. However, it requires Hilbert_Choice, which must also
> be introduced earlier. We previously put some effor
Florian has suggested making sledgehammer available earlier in the
construction of Main, before PreList at least. This could be useful
to developers. However, it requires Hilbert_Choice, which must also
be introduced earlier. We previously put some effort into making
virtually all of HOL in
On Friday 14 September 2007, Stefan Berghofer wrote:
> Lawrence Paulson wrote:
> > We previously put some effort into making
> > virtually all of HOL independent of the axiom of choice, so this
> > would be a reversal. [...] Can anybody comment?
>
> For those members of the list who have not follow
15 matches
Mail list logo
