@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
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.