Email Gateway (Aug 22 2022 at 12:59): Email Gateway (Aug 22 2022 at 12:59):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Hi
Can I use "IsarMathLib" library in Isabelle? and where I can put this
library file to work correctly with Isabelle commands like nitpick and
sledgehammer?
regards
Omar
Email Gateway (Aug 22 2022 at 13:00):From: Lars Hupel <hupel@in.tum.de>
Hi Omar,
yes, you can. IsarMathLib is a library for Isabelle.
As far as I know, it uses ZF as its underlying logic. However,
Sledgehammer and Nitpick, as they are implemented in Isabelle, require
HOL as underlying logic. That means you can't use them with IsarMathLib.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:00):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Omar,
Can I use "IsarMathLib" library in Isabelle?
Probably -- but I'll let others who know IsarMathLib and Isabelle/ZF better answer this.
and where I can put this
library file to work correctly with Isabelle commands like nitpick and
sledgehammer?
Unfortunately, Nitpick and Sledgehammer are limited to Isabelle/HOL. However, Nitpick's successor, Nunchaku, is currently being developed, and we aim at targeting set theory as well (Isabelle/TLA and Isabelle/ZF), so that it could be used in conjunction with IsarMathLib. As for Sledgehammer, we also want to generalize in the same direction, but have currently no financing or student working on that.
Cheers,
Jasmin
Last updated: Apr 24 2024 at 20:16 UTC