, x1,..., xp are variables and
F, F1,...,Fn are formulae, then the following
constructs are formulae as well.
Syntax
Semantics
-F1
Negation (not F1)
(F1 | ... | Fn)
Disjunction (F1 or ... or Fn)
(F1 & ... & Fn)
Conjunction (F1 and ... and Fn)
(F1 = ... = Fn)
Equivalence (F1 iff ... iff Fn)
(F1 # ... # Fn)
Exclusif or (F1 xor ... xor Fn)
(F1 => F2)
Implication (F1 implies F2)
(F1 <= F2)
Co-implication (F2 implies F1)
(F1 ? F2 : f3)
If F1 Then F2 Else f3
@(k,[F1,...,Fn])
k out of F1,...,Fn
#(i,j,[F1,...,Fn])
At least i and at most j out of
F1,...,Fn
exists x1,...,xp F1
Existential quantification
forall x1,...,xp F1
Universal Quantification
cofactor l1,...,lp F1
Cofactor, where li=xi or li=-xi (i=1,..,p)
x := F;
variable definition (equation)
Example
TOP := (G1 | g2);
G1 := (E1 & E2);
G2 := (E2 & E3);
The DNF Format
The DNF format for sums of products is a very simple format
in which everything is declared in advance (in order to
allocate data structures before filling them). Here follows
an introducing example.
DNF 4 3
VAR 1 a
VAR 2 b
VAR 3 c
VAR 4 d
LAW 1 0.01
PRD 3 1 -2 3
PRD 2 -4 1
PRD 2 -4 2
A description is a sequence of instructions (one per line).
A description starts with a header of the form:
DNF #variables #products
Variables are numbered from 1 to #variables.
Negative literals are just denoted with negative numbers.
It is possible to name to variables through the instruction:
VAR number name
It is possible to associate probabilities to variables through the instruction
LAW number probability
The syntax for products is as follows.
PRD size literal1 ... literalsize
The description ends with the last product declaration (otherwise
the various instructions can be given in any order).
The above description encode the sum of products
a.-b.c + -d.a + -d.b . The probability 0.01
is associated with a.