DFG2OTTER(1) SPASS DFG2OTTER(1)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
perl v5.10.0 2010-02-23 DFG2OTTER(1)
Check Out this Related Man Page
DFG2DFG(1) SPASS DFG2DFG(1)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 : spass@mpi-inf.mpg.de
perl v5.10.0 2010-02-23 DFG2DFG(1)
Hi all,
Can you please let me know how to achieve the below thing
AAABBCC@#$W123
123@#$DFG<>.
Output:
AAABBCW123
123DFG
i.e I want to filer only alphanumerics from the strings (4 Replies)
Greetings friends, I was looking for something about <i>Lua Script Language<i/> and I didn'y find anything, and then I had a thought that It'd be easy if in the Programming Topic there are subtopics with is organized by programming languages.
Just a thought (0 Replies)
One more detail, since I never was interested in netflix or hulu. But since netflix started to make it harder for so called thugs, I see in iceweasel, firefox, konqueror, qupzilla (did not try Otter or Midori) that any adblocking policy or addon just slams down my browser immediately. Only chrome... (3 Replies)