Tactics and tacticals, programs that represent and execute several steps of deduction, are fundamental to theorem provers providing automated tools for creating proofs quickly and easily. The language used for tactics is usually a full-scale programming language, separate from the language used to represent proofs. Consequently, there is also a separation between the use of theorems in proofs and the use of tactics. Our goal is to represent tactics in a way that allows them to be treated at the same level as proofs and theorems. We also want a representation that allows us to formally translate tactics into the proof steps they represent. We extend a system presented in [1,2] to represent tactics at the same level as theorems and move freely from tactics to proof steps and provide an example of its usefulness.
展开▼
