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.
Larry

> On 2 Feb 2016, at 12:00, Buday Gergely <gbuday at karolyrobert.hu> 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.