user1868607
Reputation: 2600
What is the automation support for theories other than HOL in Isabelle?
According to my scan of the Isabelle files, the Sledgehammer tool is only available for Isabelle/HOL. I'm curious about the automation of other theories in Isabelle. For instance:
- Isabelle/ZF
- Isabelle/FOL
Do they support:
- automatic provers
- SMT solvers
- specialized decision procedures
Upvotes: 2
Views: 108
Answers (1)
Slawomir K.
Reputation: 181
Isabelle/ZF does not support SMT solvers or specialized decision procedures. As for "automatic provers" I am not sure if that counts but the method auto is quite capable. In some cases it allows to prove a theorem just referencing the premises and a list of several theorems, see for example theorem bij_base_open_homeo in IsarMathLib.
Upvotes: 2
Related Questions
- Isabelle/HOL foundations
- An example of pratical application of Isabelle/HOL
- Is it possible to write non-automatic formalizations in Isar?
- Isabelle/HOL restrict codomain
- Explore finished theories in Isabelle
- I have Isabelle/HOL theory, how can I proceed with its application?
- Instantiating theorems in Isabelle
- Universal Quantification in Isabelle/HOL
- Process a theory in Isabelle/jEdit without saving it
- how to create an object logic via thf