Email Gateway (Aug 18 2022 at 14:29): Email Gateway (Aug 18 2022 at 14:29):From: Matthew Wampler-Doty <negacthulhu@gmail.com>
Dear all,
I'm formalizing a completeness theorem for a modal logic my MSc thesis
in Isabelle/HOL, and I would like to have a section outlining the
axioms and basic rules Isabelle/HOL (since it's an LCF system after
all, so there shouldn't be too many of these). I can't seem to figure
out how to find these out; they appear to be scattered across
Isabelle/Pure and Isabelle/HOL. Can someone direct me to a listing of
all the rules and axioms?
Thanks!
~Matthew P. Wampler-Doty
Email Gateway (Aug 18 2022 at 14:29):From: Tjark Weber <webertj@in.tum.de>
Matthew,
in addition to Larry's reply, and running the risk that I'm pointing out
the obvious: the (implementation of the) inference rules of Isabelle's
meta logic may be found in src/Pure/thm.ML (see
http://isabelle.in.tum.de/repos/isabelle/file/a22b09addd78/src/Pure/thm.ML).
Regards,
Tjark
Email Gateway (Aug 18 2022 at 14:30):From: Makarius <makarius@sketis.net>
See also sections 2.3 and 2.4 in
http://isabelle.in.tum.de/documentation.html
This disentangles a bit the primitive vs. derived rules that also happen
to be in our inference kernel.
Makarius
Last updated: Apr 19 2024 at 12:27 UTC