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
PROVER9(1) General Commands Manual PROVER9(1)NAME
prover9 - resolution/paramodulation theorem prover
SYNOPSIS
prover9 [options] < input-file > output-file
prover9 [options] -f input-file > output-file
DESCRIPTION
This manual page documents briefly the prover9 command.
prover9 is an automated theorem prover for first-order and equational logic. It is a successor of the otter(1) prover. prover9 uses the
inference techniques of ordered resolution and paramodulation with literal selection.
OPTIONS
A summary of options is included below.
-h View a list of command-line options.
-x Enables an experimental enhanced auto-mode. For more information consult the prover9 manual.
-p Fully parenthesize output.
-t n Constrain the search to last about n seconds. For UNIX-like systems, the `user CPU' time is used.
-f file
Take input from file instead of from standard input.
SEE ALSO mace4(1), otter(1).
On Debian systems, the manual is found in the prover9-doc package, at /usr/share/doc/prover9-doc/manual/index.html.
AUTHOR
prover9 was written by William McCune <mccune@cs.unm.edu>
This manual page was written by Peter Collingbourne <peter@pcc.me.uk>, for the Debian project (but may be used by others).
August 12, 2007 PROVER9(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)