scientific article; zbMATH DE number 65529

MaRDI QIDQ4012877zbMATH OpenFDO

Authors Matt Kaufmann, David Basin

Publication date 27 September 1992

zbMATH Keywords

Ramsey's theoremBoyer-Moore theorem proverNuprl proof development system

Mathematics Subject Classification ID

Combinatorics in computer science (68R05) Ramsey theory (05D10)

Recommendations

• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• scientific article; zbMATH DE number 4033137
• An extension of the Boyer-Moore theorem prover to support first-order quantification
• scientific article; zbMATH DE number 1086866
• A verification system for concurrent programs based on the Boyer-Moore prover
• An empirical analysis of modal theorem provers
• scientific article; zbMATH DE number 139822
• Comparison of several proof systems of intuitionistic propositional logic
• Publication:4489064
• Some experiments with a completion theorem prover

Cited in

(8)

• scientific article; zbMATH DE number 4033137 (Why is no real title available?)
• Verifying a signature architecture: a comparative case study
• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• A Ramsey theorem in Boyer-Moore logic
• Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
• CryptHOL: game-based proofs in higher-order logic
• Set theory for verification. I: From foundations to functions
• Proving Ramsey's theory by the cover set induction: A case and comparision study.

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4012877)