Research Paper #525
|The Boyeer-Moore Prover and Nuprl: an Experimental Comparison
|In proceedings of 1st Workshop on Logical Frameworks, Antibes, France, May 1990 and to appear as a chapter in the book "Logical Frameworks", Cambridge Universit
|We use an example to compare the Boyer-Moore Theorem Prover and the Nuprl Proof Development System. The respective machine verifications of a version of Ramsey's theorem illustrate similarities and differences between the two systems. The proofs are compared using both quantitative and non-quantitative measures, and we examine difficulties in making such comparisons.
|NO ONLINE COPY