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