@INCOLLECTION{Basin90b,
AUTHOR        = "David Basin and Matt Kaufmann",
TITLE         = "The Boyer-Moore Prover and Nuprl: An Experimental Comparison",
EDITOR        = "G\'erard Huet and Gordon Plotkin",
BOOKTITLE     = "Logical Frameworks",
PUBLISHER     = "Cambridge University Press",
YEAR          = 1991,
PAGES         = "90 -- 119",
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.  },
}