1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
NAME
libnormalform - First-order logic sentence canonicalisation library
SYNOPSIS
#include <libnormalform.h>
Link with -lnormalform.
DESCRIPTION
The libnormalform library provides a mechanism for expressing
first-order logic sentence and normalises them on the fly to
negation normal form, and then lets the user choose disjunctive
normal form (DNF) or conjunctive normal form (CNF).
libnormalform support all Boolean connectives: AND, OR, XOR,
IMPLY, IF, NAND, NOR, XNOR, NIMPLY, NIF, and NOT, as well as the
boolean constants TRUE and FALSE. Additionally, libnormalform
supports three standard qualifiers: the universal qualifier
(FOR ALL), the existential qualifier (THERE EXISTS), and the
unique existential (uniqueness) qualifier (THERE EXISTS ONE).
For all binary connectives, libnormalform support simply
chaining (e.g. AND(a, b, c) instead of AND(AND(a, b), c)).
For all qualifiers, libnormalform supports qualification over
an array or an associative array.
libnormalform also provides application managed boolean
variables and functions. These as well as the domains for
qualifiers can be set dynamically and the value of the
sentence can be evaluate at any time.
When libnormalform is asked to output the sentences in DNF
or CNF, it can relax parts of sentence in case the application
wants to express the sentence in a particular form but cannot
express all parts of, and therefore needs alternative that is
at least as true. While relaxing the sentence, it can eliminiate
parts of the sentence that become redundant; to be able to do
this, it queries the application for how the application
defined variables, functions and domains depend on each other.
|
