Division of Informatics
Forrest Hill & 80 South Bridge
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 |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}