A system for multi-level mathematical reasoning
Fausto Giunchiglia, Paolo Traverso · 1994
We present a system, called GETFOL, where, for any given mathematical object theory, it is possible to define a provably correct and complete metatheory MT. Theorem proving in MT can be used to build metatheoretic representations of object level proofs. Within GETFOL, these representations can be executed to prove object level theorems. Mathematical proofs can thus be built by intermixing reasoning in the object theory and reasoning in the metatheory. This provides a very flexible way to mechanize mathematical reasoning.