The Mark2 Theorem Prover
Abstract
Mark2, a general-purpose system for computer-aided reasoning, Is described. Mark2 is an equational system of reasoning implementing a higher-order logic somewhat stronger than simple type theory. It incorporates a tactic language in which tactics are represented as a kind of equational theorem, proved in much the same way as ordinary theorems. Reasoning with expressions defined by cases is a focus of the Mark2 logic. The higher order logic of Mark2 is unusual in being untyped; it is a safe version of Quine's 'New Foundations', implemented as a lamba-calculus. Documentation for the prover is attached as an appendix.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 24, 1997
- Accession Number
- ADA332793
Entities
People
- M. R. Holmes
Organizations
- Boise State University