The University of Edinburgh -
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
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.

[Search These Pages] [DAI Home Page] [Comment]