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



On Mon, 15 Feb 2010, fctk wrote:

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.

Try "/usr/local/Isabelle2009-1/build ZF" first.


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

Depends what you want to do with it. Using existing formalizations will help to get off the ground more quickly -- these things usually take a couple of years to develop.


	Makarius





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