dfg2otter(1) [debian man page]

DFG2OTTER(1)							       SPASS							      DFG2OTTER(1)

NAME

       dfg2otter - transforms DFG clause files into Otter format

SYNOPSIS

       dfg2otter [options] <infile> <outfile>

DESCRIPTION

       dfg2otter is a C-program to transform problem input files in DFG syntax into Otter syntax. It accepts all options from SPASS, although only
       a subset has an effect on translation.

       dfg2otter negates conjecture formulae of the SPASS input file before printing the Otter usable list. The SPASS conjecture formula list is
       translated into a disjunction of the negated single conjectures.  If the SPASS input file consits of clauses, these are not modified.

SEE ALSO

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

AUTHORS

       Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

       Contact : spass@mpi-inf.mpg.de

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

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)