man dfg2otter (Commandes) - transforms DFG clause files into Otter format

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

AUTHORS

Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de> Christoph Weidenbach <weidenb@mpi-sb.mpg.de>