Which Theorem Prover? A Survey of Four Theorem Provers

Abstract

When using Formal Methods to produce verified software, mathematical theorems arise 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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1990
Accession Number
ADA232147

Entities

People

  • A. Smith

Organizations

  • Royal Signals and Radar Establishment

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Adaptive Control Systems
  • Analyzers
  • Automatic
  • Automation
  • Computer Programming
  • Computers
  • Control Systems
  • Equations
  • Language
  • Manuals
  • Operating Systems
  • Programming Languages
  • Recursive Functions
  • Specifications
  • User Interface
  • User Manuals
  • Verification

Fields of Study

  • Mathematics

Readers

  • Life Cycle Cost Analysis
  • Mathematical Modeling and Probability Theory.