NAME
dfg2dfg - calculate approximations of problems
SYNOPSIS
dfg2dfg [-horn] [-monadic] [-linear] [-shallow] [infile] [outfile]
DESCRIPTION
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.
OPTIONS
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.
SEE ALSO
SPASS(1)
AUTHORS
Enno Keen
Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de>,
Christoph Weidenbach <weidenb@mpi-sb.mpg.de>