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:

Hi Bart,

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