zbMATH — the first resource for mathematics

Towards mechanical metamathematics. (English) Zbl 0616.68075
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.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI