From 4294ec0ed06ee34920c9edaeebaeb8b65c720791 Mon Sep 17 00:00:00 2001 From: Mattias Andrée Date: Fri, 19 Jul 2024 01:29:42 +0200 Subject: First commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Mattias Andrée --- README | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 README (limited to 'README') diff --git a/README b/README new file mode 100644 index 0000000..37019cc --- /dev/null +++ b/README @@ -0,0 +1,38 @@ +NAME + libnormalform - First-order logic sentence canonicalisation library + +SYNOPSIS + #include + + 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. -- cgit v1.3.1