The Formulator

Underlying Functionality

• Use of standardized axiom sets
• Aware of axiom set dependancies
• Syntax aware formula editor (emacs mode)
• Access to tptp2X and SystemOnTPTP
• Callable from other programs

GUI Interface

• Through WWW browsing
• Provides remote access
• Varying degrees of display detail

The Implementation

• User logins and saved states
• Mostly perl
• Conforming to the standards
• Will be magical