What is the automation support for theories other than HOL in Isabelle?

user_5069802 0
Viewed 94

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
isabelle
1 Answers

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.

user_37902270
Related