×

zbMATH — the first resource for mathematics

The Boyer-Moore prover and Nuprl: An experimental comparison. (English) Zbl 0799.68169
Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 89-119 (1991).
Summary: [For the entire collection see Zbl 0741.00011.]
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.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68R05 Combinatorics in computer science
05D10 Ramsey theory
Software:
Nuprl
PDF BibTeX XML Cite