Research Paper #525
|
Title: | The Boyeer-Moore Prover and Nuprl: an Experimental Comparison
|
Authors: | Basin,D; Kaufmann,M
|
Date: | 1991
|
Presented: | 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
|
Keywords: |
|
Abstract: | 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.
|
Download: | NO ONLINE COPY
|