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



Isabelle is certainly one of the best tools you could adopt for this purpose. Isabelle supports a number of different logics, including higher order logic (Isabelle/HOL) and axiomatic set theory (Isabelle/ZF).

It isn't immediately clear from your message whether by "set theory" you are referring to heavy-duty set theoretic concepts such as ordinals and cardinals, or only simpler ones like unions and power sets. The other crucial question is whether you want your set theory to be typed or not. Higher order logic is essentially first order logic extended with functions and a simple typed set theory. For untyped, heavy-duty set theory, choose Isabelle/ZF; otherwise, choose Isabelle/HOL.
Larry Paulson


On 14 Feb 2010, at 10:34, 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?






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