dfg2dfg(1) [debian 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)
Check Out this Related Man Page
RNDC.CONF(5) BIND9 RNDC.CONF(5) NAME
rndc.conf - rndc configuration file SYNOPSIS
rndc.conf DESCRIPTION
rndc.conf is the configuration file for rndc, the BIND 9 name server control utility. This file has a similar structure and syntax to named.conf. Statements are enclosed in braces and terminated with a semi-colon. Clauses in the statements are also semi-colon terminated. The usual comment styles are supported: C style: /* */ C++ style: // to end of line Unix style: # to end of line rndc.conf is much simpler than named.conf. The file uses three statements: an options statement, a server statement and a key statement. The options statement contains five clauses. The default-server clause is followed by the name or address of a name server. This host will be used when no name server is given as an argument to rndc. The default-key clause is followed by the name of a key which is identified by a key statement. If no keyid is provided on the rndc command line, and no key clause is found in a matching server statement, this default key will be used to authenticate the server's commands and responses. The default-port clause is followed by the port to connect to on the remote name server. If no port option is provided on the rndc command line, and no port clause is found in a matching server statement, this default port will be used to connect. The default-source-address and default-source-address-v6 clauses which can be used to set the IPv4 and IPv6 source addresses respectively. After the server keyword, the server statement includes a string which is the hostname or address for a name server. The statement has three possible clauses: key, port and addresses. The key name must match the name of a key statement in the file. The port number specifies the port to connect to. If an addresses clause is supplied these addresses will be used instead of the server name. Each address can take an optional port. If an source-address or source-address-v6 of supplied then these will be used to specify the IPv4 and IPv6 source addresses respectively. The key statement begins with an identifying string, the name of the key. The statement has two clauses. algorithm identifies the encryption algorithm for rndc to use; currently only HMAC-MD5 is supported. This is followed by a secret clause which contains the base-64 encoding of the algorithm's encryption key. The base-64 string is enclosed in double quotes. There are two common ways to generate the base-64 string for the secret. The BIND 9 program rndc-confgen can be used to generate a random key, or the mmencode program, also known as mimencode, can be used to generate a base-64 string from known input. mmencode does not ship with BIND 9 but is available on many systems. See the EXAMPLE section for sample command lines for each. EXAMPLE
options { default-server localhost; default-key samplekey; }; server localhost { key samplekey; }; server testserver { key testkey; addresses { localhost port 5353; }; }; key samplekey { algorithm hmac-md5; secret "6FMfj43Osz4lyb24OIe2iGEz9lf1llJO+lz"; }; key testkey { algorithm hmac-md5; secret "R3HI8P6BKw9ZwXwN3VZKuQ=="; }; In the above example, rndc will by default use the server at localhost (127.0.0.1) and the key called samplekey. Commands to the localhost server will use the samplekey key, which must also be defined in the server's configuration file with the same name and secret. The key statement indicates that samplekey uses the HMAC-MD5 algorithm and its secret clause contains the base-64 encoding of the HMAC-MD5 secret enclosed in double quotes. If rndc -s testserver is used then rndc will connect to server on localhost port 5353 using the key testkey. To generate a random secret with rndc-confgen: rndc-confgen A complete rndc.conf file, including the randomly generated key, will be written to the standard output. Commented-out key and controls statements for named.conf are also printed. To generate a base-64 secret with mmencode: echo "known plaintext for a secret" | mmencode NAME SERVER CONFIGURATION
The name server must be configured to accept rndc connections and to recognize the key specified in the rndc.conf file, using the controls statement in named.conf. See the sections on the controls statement in the BIND 9 Administrator Reference Manual for details. SEE ALSO
rndc(8), rndc-confgen(8), mmencode(1), BIND 9 Administrator Reference Manual. AUTHOR
Internet Systems Consortium COPYRIGHT
Copyright (C) 2004, 2005, 2007 Internet Systems Consortium, Inc. ("ISC") Copyright (C) 2000, 2001 Internet Software Consortium. BIND9 June 30, 2000 RNDC.CONF(5)