For most proof assistants the name alone is common, E.g. Coq, Lean but with Isabelle it is often seen as Isabelle/<xyz>?
Why the two parts?
What is
- Isabelle/HOL
- Isabelle/FOL
- Isabelle/ZF
- Isabelle/ISAR
- Isabelle/Proof General
Are there others?
$\begingroup$
$\endgroup$
0
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
6
Isabelle the program is designed as a "generic" LCF-style proof assistant/logical framework; it gives you a very minimal base logic (based on Church's simple type theory (pdf) and called Isabelle/Pure) and some infrastructure to declare new types, typeclasses (ref), constants, and judgment forms, postulate new axioms and rules, and basic tactics for performing logical reasoning therein.
Using this logical framework, and writing ML code (Poly/ML) to interface with it, one can develop object logics (pdf) and other applications x within Isabelle; these are then called "Isabelle/x".
x = HOL, FOL, ZF, ... are object logics, they encode the rules of the particular logic in the language of Isabelle/Pure, and extend the framework with extra functionality for e.g. defining recursive functions, new tactics, theory libraries of formalizations, etc.
x = Isar is an extension of the original Isabelle framework to allow for declarative proofs; it's now been very tightly integrated into Isabelle, but in the beginning proofs were done tactic-style, similar to how it's still done (I believe) in the HOL family of ITPs.
x = Proof General is, I assume, the PG interface of the Isabelle prover.
To name a couple more interesting applications, there's Isabelle/auto2 by Bohua Zhan, it's a saturation-based theorem prover tool that enables very declarative proofs that don't require explicit tactic invocations after each claim. This allows for proofs that read quite similar to ones on paper, see e.g. here.
I myself have tried to develop HoTT as an object logic, but it's not currently being actively worked on.
I suppose this is similar to how Metamath works, but I'm not an expert on that.
-
$\begingroup$ I was finishing my own answer when yours appeared. I'm leaving it for a while just in case $\endgroup$ Feb 17, 2022 at 12:08
-
1$\begingroup$ Very minor but mildly important squabble: I would push back a little, and point out that Isabelle is a meta-logical framework (which is stronger than "just" a logical framework because we can prove results about the object logic, whereas logical frameworks only facilitate reasoning within an object logic). (But this is an excellent answer, otherwise a minor point about a prefix.) $\endgroup$ Feb 17, 2022 at 20:36
-
$\begingroup$ @GuyCoder I'm ready: what're your queries? $\endgroup$ Feb 17, 2022 at 23:02
-
$\begingroup$ @GuyCoder I believe this is answered in "Rewriting logic as a metalogical framework" by David Basin, Manuel Clavel, and Jos Meseguer; the tl;dr is Isabelle does not provide sufficient mechanization of induction on its own, whereas Isabelle/HOL does. $\endgroup$ Feb 18, 2022 at 16:24
-
1$\begingroup$ @GuyCoder Please keep extended discussions out of answer comments :) $\endgroup$– JoshFeb 18, 2022 at 16:41
$\begingroup$
$\endgroup$
0
There are many more, notably:
- Isabelle/Pure (the core logic),
- Isabelle/jEdit (the bundled IDE),
- Isabelle/ML (its version of the ML language and its libraries),
- Isabelle/Scala (same for Scala),
I believe that one of the main reasons for this is that Isabelle was designed as a generic proof assistant: not committed to any particular (strong) logical foundation. Its core essentially manages “meta-rules” and on top of that you can define the rules proper (and axioms) of the formal system of your choice. Thus, in many of the examples above, the compound name refers to the logic that you are using (HOL, FOL, ZF = FOL + a type for sets + ZF axioms, or even just the basic core Pure).
A second (a bit idiosyncratic?) reason that involves the software design of Isabelle is that the software consists of a really big bundle of many components, some of which are especially tailored to work together---instead of using some standard version appearing among the packages offered by any particular operative system. I understand that the IDE jEdit originated independently, but it is highly customized to work with Isabelle. Also, Isabelle include its own libraries for ML and Scala, its own Java environment, and specific versions of the SMT solvers (E, Vampire, Z, etc).
answered Feb 17, 2022 at 12:05