Griffin, Timothy G.2007-04-232007-04-231987-06http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-846https://hdl.handle.net/1813/6686This report describes the Environment for Formal Systems, 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.2718723 bytes619415 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report