×

A mechanical proof of the Church-Rosser theorem. (English) Zbl 0654.68103

A frequent argument against automated theorem proving is its weakness in proving larger and more substantial mathematical theorems. However, it was already shown by L. Wos, S. Winker and B. Smith [Artif. Intell. 22, 303-356 (1984; Zbl 0553.68051)], how to use a theorem prover to prove previously unsolved problems in equivalence logic.
In this paper the author demonstrates the power of the Boyer-Moore theorem prover [R. S. Boyer and J. S. Moore, A computational logic (1979; Zbl 0448.68020)] in proof checking a proof of the famous Church-Rosser theorem of combinatory logic. Proof checking essentially means, that local parts of the proof are proved automatically, but the global structure of the proof is given in advance. Technically, the proof is based on Tait and Martin-Löf and involves the use of de Bruijn’s notation for \(\lambda\)-calculus; to use de Bruijn’s notation in the Boyer-Moore theorem prover, a mechanical language transformation was performed.
A very interesting feature of the formalized and mechanical proof version is, that some of the lemmas (the diamond property of walks) got a shorter and even clearer proof than in the informal framework of “hand”- mathematics. The well written paper (it gives an introduction to all required concepts) represents a further success achieved by the use of computers in doing mathematics (even metamathematics and logic); the outcome is not only verification itself, but also an extended insight into the structure of proofs and formalisms.
Reviewer: A.Leitsch

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI