Transforms dfg clause files into otter format
dfg2otter [options] <infile> <outfile>
dfg2otter is a C-program to transform problem input files in \s-1DFG\s0 syntax into Otter syntax. It accepts all options from \s-1SPASS\s0, although only a subset has an effect on translation.
dfg2otter negates conjecture formulae of the \s-1SPASS\s0 input file before printing the Otter usable list. The \s-1SPASS\s0 conjecture formula list is translated into a disjunction of the negated single conjectures. If the \s-1SPASS\s0 input file consits of clauses, these are not modified.
checkstat\|(1), filestat\|(1), pcs\|(1), pgen\|(1), rescmp\|(1), tpform\|(1), tpget\|(1), deprose\|(1), dfg2otter.pl\|(1), \s-1SPASS\s0\|(1)
Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach
Contact : [email protected]