Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer

Isabelle/ZF is surely best for developments in axiomatic set theory. But there is no sledgehammer there.

> On 2 Feb 2016, at 12:00, Buday Gergely <gbuday at> wrote:
>> Isabelle/HOL introduces the axiom of choice fairly late in the development
>> (contrast with other HOL implementations, which include it as part of the
>> basic axiomatic set up), but from that point onwards, it gets intertwined with
>> everything. It would be better if you chose a development involving AC,
>> something to do with cardinals perhaps, or simply some of the more obscure
>> consequences of AC.
> Her research page tells me that her research goal is especially discovering how far one can get without the axiom of choice.
> Might it be that Isabelle/ZF is better for her aim?

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