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



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.