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