Towards mechanical metamathematics (Q1821563)

Metamathematics is a source of many ineresting theorems and difficult proofs. This paper reports the results of an experiment to use the Boyer- Moore theorem prover to proof-check theorems that the prover was able to prove about this logic. These include the tautology theorem which states that every tautology has a proof. Such proofs can be used to add new proof procedures to a proof-checking program in a sound and efficient manner.