formed(1) [debian man page]
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
ANLDP(1) General Commands Manual ANLDP(1) NAME
anldp - implementation of Davis-Putnam propositional satisfiability procedure SYNOPSIS
anldp [options] < input-file > output-file DESCRIPTION
This manual page documents briefly the anldp command. anldp is an implementation of a Davis-Putnam procedure for the propositional satisfiability problem. anldp exposes the procedure used by mace2(1) to determine satisfiability. anldp can also take statements in first-order logic with equality and a domain size n then search for models of size n. The first-order model-searching code transforms the statements into set of propositional clauses such that the first- order statements have a model of size n if and only if the propositional clauses are satisfiable. The propositional set is then given to the Davis-Putnam code; any propositional models that are found can be translated to models of the first-order statements. The first-order model-searching program accepts statements only in a flattened relational clause form without function symbols. OPTIONS
-s Perform subsumption. (Subsumption is always performed during unit preprocessing.) -p Print models as they are found. -m n Stop when the nth model is found. -t n Stop after n seconds. -k n Allocate at most n kbytes for storage of clauses. -x n Quasigroup experiment n. -B file Backup assignments to a file. -b n Backup assignments every n seconds. -R file Restore assignments from a file. The file typically contains just the last line of a backup file. Other input, in particular the clauses, must be given exactly as in the original search. -n n This option is used for first-order model searches. The parameter n specifies the domain size, and its presence tells the program to read first-order flattened relational input clauses instead of propositional clauses. SEE ALSO
formed(1), mace2(1), otter(1). Full documentation for anldp is found in /usr/share/doc/mace2/anldp.{html,ps.gz}. AUTHOR
anldp 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 ANLDP(1)