Re: [isabelle] Setting up a logic: need instructions.
My first priority is not to actually set up a new logic, but to understand
how this one is set up. I am working inside ZF, and am trying to
understand how the system works in the background. It seems to me that
knowing what these "incantations" really do to the system is important for
this. Also to learn to use the system more effectively. I am also
learning SML for this (and maybe to write some extensions at some point),
but I have not found a good entrance point into the code yet.
Btw, I do like HOL but the current project if formalizing a result from
set theory itself. Using ZF for this does seem more natural.
On Thu, 25 Feb 2010, Tobias Nipkow wrote:
I would be interested why you feel it necessary to set up a new logic.
To get anywhere requires an enormous amount of ground work. I can
understand that as a mathematician you may not like HOL, but ZF might be
more to your taste - and although not as well developed as HOL, it is
still a lot better than nothing.
Bart Kastermans wrote:
I am trying to better understand how logics that come with Isabelle are
set up, and how to set up my own. Is there any good documentation on
this? Explaining the use of TrueProp, and say all the commands in the
first 150 lines of a file like IFOL.thy .
This archive was generated by a fusion of
Pipermail (Mailman edition) and