FormEd: An X Window System application for managing first-order formulas
T.L. Henry, William W. McCune · 1990
FormEd is a window-based program for constructing, displaying, and managing first-order logic formulas. The main motivation for constructing FormEd was the desire to have formulas displayed in a readable, two-dimensional format. Users of FormEd can make two kinds of transformation on formulas: logic transformations, such as negation normal form translation, which preserve the meaning of a formula, and edit transformations, which can be used to make arbitrary changes, such as adding a hypothesis to a subformula. FormEd was written by using the X Window System, Version 11, and code from the theorem prover OTTER. 4 refs.