First commit

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

1 files changed, 94 insertions, 0 deletions

diff --git a/libnormalform.7 b/libnormalform.7
new file mode 100644
index 0000000..1607b34
--- /dev/null
+++ b/libnormalform.7
@@ -0,0 +1,94 @@
+.TH LIBNORMALFORM 7 LIBNORMALFORM
+.SH NAME
+libnormalform \- First-order logic sentence canonicalisation library
+
+.SH SYNOPSIS
+.nf
+#include <libnormalform.h>
+
+LIBNORMALFORM_SENTENCE *libnormalform_true(void);
+LIBNORMALFORM_SENTENCE *libnormalform_false(void);
+LIBNORMALFORM_SENTENCE *libnormalform_variable(struct libnormalform_variable *);
+LIBNORMALFORM_SENTENCE *libnormalform_function(struct libnormalform_function *);
+LIBNORMALFORM_SENTENCE *libnormalform_transformation(struct libnormalform_transformer *, LIBNORMALFORM_SENTENCE *);
+
+LIBNORMALFORM_SENTENCE *libnormalform_not(LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_and(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_or(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_xor(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_imply(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_if(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_nand(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_nor(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_xnor(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_nimply(LIBNORMALFORM_SENTENCE **);
+LIBNORMALFORM_SENTENCE *libnormalform_nif(LIBNORMALFORM_SENTENCE **);
+
+LIBNORMALFORM_SENTENCE *libnormalform_all(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_any(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_one(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_exists(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_nexists(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_unique(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_existentially(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_universally(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_uniquely(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_empty(struct libnormalform_map *);
+LIBNORMALFORM_SENTENCE *libnormalform_nonempty(struct libnormalform_map *);
+LIBNORMALFORM_SENTENCE *libnormalform_singleton(struct libnormalform_map *);
+
+LIBNORMALFORM_SENTENCE *libnormalform_ref(LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_clone(LIBNORMALFORM_SENTENCE *);
+void libnormalform_free(LIBNORMALFORM_SENTENCE *);
+
+char *libnormalform_to_string(LIBNORMALFORM_SENTENCE *);
+LIBNORMALFORM_SENTENCE *libnormalform_from_string(char *, char **, const struct libnormalform_representation_spec *);
+
+int libnormalform_evaluate(LIBNORMALFORM_SENTENCE *);
+struct libnormalform_term *libnormalform_dnf(LIBNORMALFORM_SENTENCE *, uint64_t);
+struct libnormalform_term *libnormalform_cnf(LIBNORMALFORM_SENTENCE *, uint64_t);
+struct libnormalform_term *libnormalform_express(LIBNORMALFORM_SENTENCE *, uint64_t);
+.fi
+.PP
+Link with
+.IR -lnormalform .
+
+.SH DESCRIPTION
+The
+.B 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).
+.PP
+.B 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,
+.B 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.
+.P
+.B 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.
+.PP
+When
+.B 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.
+.SH SEE ALSO
+None.