Which Theorem Prover. A Survey of Four Theorem Provers

摘要

When using Formal Methods to produce verified software, mathematical theoremsarise which need to be proved. This memorandum contains the experience gained in using four theorem provers to prove such theorems. From this experience, a number of recommendations are made on what constitutes a good theorem prover. (Author)