On February 16, 2023 at 14:00 EET, Ionuț Țuțu (Simion Stoilow Institute of Mathematics of the Romanian Academy) will give a talk in the Logic Seminar.
Title: A short guide to implementing theorem provers
Abstract: 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 some 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. Our effort is supported by SpeX, a rewrite-based environment that facilitates the development of formal-specification languages and tools.
The talk will take place physically at FMI Hall 214 “Google”.