FORMED(1) General Commands Manual FORMED(1)NAME
formed - formula editor for first-order logic formulas
SYNOPSIS
formed [options]
DESCRIPTION
This manual page documents briefly the formed command.
formed is a window-based program for constructing, displaying, and managing first-order logic formulas. The main motivation for construct-
ing formed was the desire to have formulas displayed in a readable, two-dimensional format. Users of formed can make two kinds of transfor-
mation 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. formed was written by using
the X Window System, Version 11, and code from the theorem prover otter.
OPTIONS
A summary of options is included below.
-l filename
Load formulas in the specified file during startup. Formulas can also be loaded after startup with the button Load in the main menu.
-f color
Use the named color for the foreground on color monitors (ignored on black-and-white monitors).
-b color
Use the named color for the background on color monitors (ignored on black-and-white monitors).
SEE ALSO anldp(1), mace2(1), otter(1).
``FormEd: An X Window System application for managing first-order formulas'' (McCune et al.), available from http://www.osti.gov/energyci-
tations/servlets/purl/6427100-WtOa4g/6427100.PDF
AUTHOR
formed ws written by William McCune <otter@mcs.anl.gov>
This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by others).
November 5, 2006 FORMED(1)
Check Out this Related Man Page
OTTER(1) General Commands Manual OTTER(1)NAME
otter - resolution-style theorem prover
SYNOPSIS
otter < input-file > output-file
DESCRIPTION
This manual page documents briefly the otter command.
otter is a resolution-style theorem-proving program for first-order logic with equality. otter includes the inference rules binary resolu-
tion, hyperresolution, UR-resolution, and binary paramodulation. Some of its other abilities and features are conversion from first-order
formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation,
evaluable functions and predicates, Knuth-Bendix completion, and the hints strategy.
OPTIONS
No command-line options are accepted; all options are given in the input file.
SEE ALSO anldp(1), formed(1), mace2(1).
Full documentation for otter is found in /usr/share/doc/otter/otter33.{html,ps.gz}.
AUTHOR
otter ws written by William McCune <otter@mcs.anl.gov>
This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by others).
November 5, 2006 OTTER(1)
Im trying to create a utility that can do unit conversions using a seperate formula file(one which i can add conversions to at a later date). however i'm stuck when it comes to pulling the formulas out of the formula file for use in the script.
heres a rundown of what the script does.
The... (4 Replies)
Hello!:) There is the following situation: I've got video Ti 4200 on FreeBSD 5.1 and two monitors connected to it, how can I make available the second monitor in CLI and GUI. Thanks! (0 Replies)
:confused:How do I configure Solaris 11 to use both my elite 3d cards and monitors to create one big screen? My machine is an Ultra80:confused: (2 Replies)
I am searching for some logic which will help me to introduce quick action for the errors. We have application server and we need to check the bunch of information for every 10 minutes and alert thru mail. I wrote a script in which i am tailing last 1000 lines and counting one exception then... (21 Replies)
I am trying to get AIX CDE to run with dual monitors. I just upgraded to my desktop to use dual monitors. When I log in to my AIX system with exceed running and issue the Xsession command the Splash screen flash on 1 screen then disappears but the desktop never shows. How do I set up Xsession to... (1 Reply)
I am using below logic to validate whether i am expecting the correct data from source,if not logic should give which column has error.i am running below logic in linux
awk -F, '
NR==1{next}
{f=" "}
$1!~/^{0,5}$|^$/{f=f?f" emp_id-error":"emp_id-error"}
$4!~/^{0,6}$|^$/{f=f?f"... (4 Replies)