First commit

Signed-off-by: Mattias Andrée <maandree@kth.se>

1 files changed, 38 insertions, 0 deletions

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 <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.