diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 38 |
1 files changed, 38 insertions, 0 deletions
@@ -0,0 +1,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. |