.TH FORMED 1 "November 5, 2006" .SH NAME formed \- formula editor for first-order logic formulas .SH SYNOPSIS .B formed .RI [ options ] .SH DESCRIPTION This manual page documents briefly the .B formed command. .PP \fBformed\fP is a window-based program for constructing, displaying, and managing first-order logic formulas. The main motivation for constructing \fBformed\fP was the desire to have formulas displayed in a readable, two-dimensional format. Users of \fBformed\fP can make two kinds of transformation on formulas: (1) logic transformations, such as negation normal form translation, which preserve the meaning of a formula, and (2) edit transformations, which can be used to make arbitrary changes, such as adding a hypothesis to a subformula. \fBformed\fP was written by using the X Window System, Version 11, and code from the theorem prover \fBotter\fP. .SH OPTIONS A summary of options is included below. .TP .B \-l \fIfilename Load formulas in the specified file during startup. Formulas can also be loaded after startup with the button \fBLoad\fP in the main menu. .TP .B \-f \fIcolor Use the named color for the foreground on color monitors (ignored on black-and-white monitors). .TP .B \-b \fIcolor Use the named color for the background on color monitors (ignored on black-and-white monitors). .SH SEE ALSO .BR anldp (1), .BR mace2 (1), .BR otter (1). .br ``FormEd: An X Window System application for managing first-order formulas'' (McCune et al.), available from http://www.osti.gov/energycitations/servlets/purl/6427100-WtOa4g/6427100.PDF .SH AUTHOR \fBformed\fP ws written by William McCune .PP This manual page was written by Peter Collingbourne , for the Debian project (but may be used by others).