Paul Y. Gloess. An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions. In Wolfgang Bibel, Robert A. Kowalski, editors, 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings. Volume 87 of Lecture Notes in Computer Science, pages 154-169, Springer, 1980.
Abstract is missing.