.TH LIBNORMALFORM 7 LIBNORMALFORM
.SH NAME
libnormalform \- First-order logic sentence normalisation 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.