@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Template for ARS database entries
==============================================================================
Name: Mark2 (officially "EFTTP Mark 2")
Keywords: equational interactive tactics
Description:
Semantics:
equational logic; there is a higher order logic
underlying the definition facility which can be
thought of as a polymorphic version of a fragment of
Church's simple type theory (it is actually a version
of Quine's set theory New Foundations adapted to
functions), but the role of this higher order logic is
auxiliary.
Deductive machinery:
Reasoning is strictly equational and user-controlled.
The user can develop proof tactics.
Dynamics:
Proofs are developed by manipulating terms using
equational theorems as rewrite rules on specified
subterms. New theorems (equations) can be
proven and stored in theories. Proof tactics are
represented internally as equational theorems (there's
a trick to this!), "proved" and stored in the same way
as theorems. The basic proof procedure is quite
laborious, but the tactic language redeems it.
Persistence:
Theories can be saved and restored. Theories include
equational theorems, proof tactics represented as
equational theorems and theorems under development as
well. Proofs are not stored but dependencies of
theorems (and tactics) on axioms are stored.
Interpretations of one theory in another can be
specified and used to export theorems and tactics.
Contact persons:
Randall Holmes at Boise State University
(holmes@math.idbsu.edu)
phone 1-208-345-2899
User group:
Just myself, so far. I'd be happy to advise anyone
who wants to try it out. A publication is my "Disguising
recursively chained rewrite rules as equational
theorems, as implemented in the prover EFTTP Mark2" in
Lecture Notes in Computer Science vol. 914
(proceedings of RTA '95), Springer-Verlag 1995. This
work is supported by grant number DAAH04-94-G-0247
from the US Army Research Office.
Pragmatics:
I don't have much basis for comparison; I'll have a
better idea when there are users.
Documentation:
Very limited! What there is is present on the WWW
page. This is a main focus of my effort at the
moment.
Applications:
None so far.
Extensions/enhancements:
Resource requirements:
Implemented in Standard ML of New Jersey.
Continuously under development! There is a fairly
good partial implementation in Caml Light and a
fragment of an implementation in C++.
Where-to-get-it:
From my WWW page (SML source code):
http://math.idbsu.edu/faculty/holmes.html
One should look for updates frequently; version notes
are provided on the WWW page.
[Info source, date]
Randall Holmes, Aug. 23, 1995.