dfg2otter.pl(1) [debian man page]

DFG2OTTER.PL(1) 						       SPASS							   DFG2OTTER.PL(1)

NAME

       dfg2otter - transforms DFG clause files into Otter format including Otter options

SYNOPSIS

       dfg2otter.pl [options] [infile] [outfile]

DESCRIPTION

       dfg2otter.pl is a Perl wrapper for the dfg2otter. Mainly, it adds a set of OTTER parameters to the transformation result of dfg2otter.
       Additionally, input/output redirection is simpler: If no file arguments are given, dfg2otter.pl reads from stdin and writes to stdout. If
       one file argument is given, dfg2otter.pl read from that file, and if a second argument is present, dfg2otter.pl writes to it.

OPTIONS

       -t n
	   Sets the time limit for the OTTER proof attempt to n seconds.

SEE ALSO

       checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), SPASS(1)

AUTHORS

       Thorsten Engel and Christian Theobalt.

       Contact : spass@mpi-inf.mpg.de

perl v5.10.0							    2010-02-23							   DFG2OTTER.PL(1)

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)