## An Environment for Formal Systems

**T.G. Griffin**
*Abstract:* This report describes the *E*nvironment
for *F*ormal *S*ystems, EFS, that allows a user to
interactively define the syntax and inference rules of a formal
system and to construct proofs in the defined system. The EFS
supports two AUTOMATH-like formalisms for encoding logics: the
Edinburgh Logical Framework and the Calculus of Constructions.
Facilities are provided for the definition of notational
abbreviations and the construction of goal-directed proofs. New
goal-directed rules can be interactively defined and checked for
validity. The EFS was implemented with the Cornell Synthesizer
Generator.

*LFCS report ECS-LFCS-87-34*

Previous |

Index |

Next