Re: [isabelle] Is Isabelle the right tool for me?



Thanks for your answer. Anyway I have a problem at installing
Isabelle/ZF in that, after having unpacked the bundle and ZF under
/usr/local, I can't run isabelle tty. It says:

/usr/local/Isabelle2009-1/bin$ ./isabelle tty
Unknown logic "ZF" -- no heap file found in:
  /home/francesco/.isabelle/heaps/Isabelle2009-1/polyml_x86-linux
  /usr/local/Isabelle2009-1/heaps/polyml_x86-linux

It tries to find ZF instead of HOL because I edited ISABELLE_LOGIC
variable in etc/settings.

Also, why do I need an already built set theory? My goal is to write
set theory from scratch. I'd like to use only the rules of inference
of first order logic (natural deduction).

On 15 February 2010 10:30, Makarius <makarius at sketis.net> wrote:
> On Sun, 14 Feb 2010, fctk wrote:
>
>> I'd like to use a proof assistant in order to formalize elementary
>> theorems from set theory. I think I just need some tool that understands the
>> rules of inference of natural deduction for first-order logic.
>>
>> Is Isabelle the right tool for me?
>
> Yes, see Isabelle/ZF.  This page by one of our users provides a nice intro,
> and additional libraries: http://www.nongnu.org/isarmathlib
>
>
>        Makarius





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