diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform.7 | 94 |
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. |