dfg2dfg - calculate approximations of problems

**dfg2dfg** [-horn] [-monadic] [-linear] [-shallow] [

*infile*]
[

*outfile*]

**dfg2dfg** is a program that reads clauses from an input file in DFG syntax.
It then calculates an approximation of the clause set depending on the command
line options. Finally it writes the approximated clause set in DFG syntax to a
file.

If neither

*infile* nor

*outfile* are given,

**dfg2dfg** reads from
standard input and writes to standard output. If one file name is given, it
reads from that file and writes the output to standard output. If more than
one file name is given,

**dfg2dfg** reads from the first file and writes to
the second.

The approximations are described in technical detail in the separate paper

**dfg2dfg.ps** included in the SPASS distribution.

**dfg2dfg** has four different command line options that may be combined.

- -horn
- This option enables the transformation of non-horn clauses
into horn clauses. Each non-horn clause with
*n* positive literals is
transformed into *n* horn clauses, where the *i*-th clause
contains the *i*-th positive literal and all negative literals of the
non-horn clause. See also section 3 of the paper.

- -monadic[=n]
- With this option atoms with non-monadic predicate symbols
are transformed into monadic atoms. If
*n* is omitted or *n*=1 a
term encoding is applied, i.e., all non-monadic predicates are moved to
the term level. With *n*=2 a projection is applied. All non-monadic
atoms are replaced by their monadic argument projections. See section 4.1
section 4.2 of the paper for more details.

- -linear
- This approximation transforms a clause with monadic
literals and non-linear variable occurrences in succedent atoms, into a
new clause with possibly more negative literals, that doesn't contain any
non-linear variables in the succedent. See section 5 of the paper for
details.

- -shallow[=n]
- This transformation tries to reduce the depth of the terms
in positive literals. The transformation is applied to horn clauses with
monadic literals only. If
*n* is omitted or *n*=1 a strict
transformation is applied, that is equivalence preserving, however. For
*n*=2 some preconditions are removed. This allows the transformation
to be applied more often, but the transformation isn't equivalence
preserving any more. For *n*=3 even more preconditions are removed.
Take a look at section 6. *n* of the paper for the details of the
command line option *-monadic=n*.

*SPASS*(1)

Enno Keen

Contact : spass@mpi-inf.mpg.de