An introduction to experimental theorem proving

We briefly venture into the world of experimental theorem proving to see what it takes to bring proof calculi to life, making them readily available for teaching and for further research purposes. In contrast to many mainstream theorem provers such as E, Vampire, Gandalf, Isabelle, or Lean, which are based on specific logics or families of logics, the approach we propose here is generic. That is, we separate those aspects of a theorem prover that are language independent (e.g., basic proof management) from aspects that are language dependent, such as the base logical system(s) or the kind of inference rules used in proofs. The results presented in this talk are supported by and fully integrated into SpeX, a rewrite-based logical environment that facilitates the development of emergent formal-specification languages and tools.

Ionuț Țuțu

Last modified: Wed Nov 29 21:51:34 EET 2023