Defcnf (Calculemus)

Defcnf Module

Namespace: Calculemus
Assembly: Calculemus.dll

Definitional Conjunctive Normal Form.

Table of contents

Core definitional CNF procedure
Overall definitional CNF
Optimized definitional CNF
3-CNF

Core definitional CNF procedure

Functions and values

Function or value	Description
`defstep op (p, q) (fm, defs, n)` Full Usage: `defstep op (p, q) (fm, defs, n)` Parameters: op : `formula<prop> -> formula<prop> -> formula<prop>` - The binary formula constructor received from maincnf. p : `formula<prop>` - The left-hand sub-formula. q : `formula<prop>` - The right-hand sub-formula. fm : `formula<prop>` - The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` - The definitions made so far. n : `bigint` - The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index.	Used to define Defcnf.maincnf. op : `formula<prop> -> formula<prop> -> formula<prop>` The binary formula constructor received from maincnf. p : `formula<prop>` The left-hand sub-formula. q : `formula<prop>` The right-hand sub-formula. fm : `formula<prop>` The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` The definitions made so far. n : `bigint` The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index.
`maincnf (fm, defs, n)` Full Usage: `maincnf (fm, defs, n)` Parameters: fm : `formula<prop>` - The formula to be transformed (supposed to be already in Prop.nenf). defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` - The definitions made so far. n : `bigint` - The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index.	Core definitional CNF procedure. fm : `formula<prop>` The formula to be transformed (supposed to be already in Prop.nenf). defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` The definitions made so far. n : `bigint` The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index. Example `maincnf (!> @"p \/ (p \/ q)", undefined, 0I) \|> fun (fm,defs,counter) -> fm, defs \|> graph, counter` val fm: obj val defs: obj val counter: obj Evaluates to: `("p_1", [("p \/ p_0", ("p_1", "p_1 <=> p \/ p_0")); ("p \/ q", ("p_0", "p_0 <=> p \/ q"))], 2I)`
`mkprop n` Full Usage: `mkprop n` Parameters: n : `bigint` - The index of the variable. Returns: `formula<prop> * bigint` The indexed variable and the next index	Generates an indexed variable of the form `p_n` and the next index `n+1`. n : `bigint` The index of the variable. Returns: `formula<prop> * bigint` The indexed variable and the next index Example `mkprop 3I` Evaluates to (`p_3`, 4 {IsEven = true; IsOne = false; IsPowerOfTwo = true; IsZero = false; Sign = 1;})

Overall definitional CNF

Functions and values

Function or value	Description
`defcnf01 fm` Full Usage: `defcnf01 fm` Parameters: fm : `formula<prop>` - The input formula. Returns: `formula<prop>` An equisatisfiable CNF of the input formula.	Returns an equisatisfiable CNF of the input formula using a definitional procedure, transforming each definition in isolation. fm : `formula<prop>` The input formula. Returns: `formula<prop>` An equisatisfiable CNF of the input formula. Example `!>"p ==> q" \|> defcnf01` Evaluates to `(p \/ p_1) /\ p_1 /\ (p_1 \/ ~q) /\ (q \/ ~p \/ ~p_1)`.
`max_varindex pfx s n` Full Usage: `max_varindex pfx s n` Parameters: pfx : `string` - The prefix to be checked. s : `string` - The input variable name. n : `bigint` - The value to compare. Returns: `bigint` If `s` is of the form `pfx_m` returns the larger between `m` and `n`; otherwise `n`.	Return the larger between `n` and the index `m` of the variable `s` if this is of the form `pfx_m`. pfx : `string` The prefix to be checked. s : `string` The input variable name. n : `bigint` The value to compare. Returns: `bigint` If `s` is of the form `pfx_m` returns the larger between `m` and `n`; otherwise `n`. Example `max_varindex "p_" "p_0" 1I // evaluates to 1I max_varindex "p_" "p_2" 1I // evaluates to 2I max_varindex "p_" "x_2" 1I // evaluates to 1I`
`mk_defcnf fn fm` Full Usage: `mk_defcnf fn fm` Parameters: fn : `formula<prop> * func<'a, 'b> * bigint -> formula<'c> * func<'d, ('e * formula<'c>)> * 'f` - The specific definitional CNF procedure. fm : `formula<prop>` - The input formula. Returns: `formula<'c> list list` The CNF result of `fn` in a set-of-sets representation.	Returns the result of a specific CNF procedure in a set-of-sets representation. Transforms a generic propositional formula `fm` in Prop.nenf and then it applies to the result a specific definitional CNF procedure `fn` returning an equisatisfiable CNF in a set-of-sets representation. fn : `formula<prop> * func<'a, 'b> * bigint -> formula<'c> * func<'d, ('e * formula<'c>)> * 'f` The specific definitional CNF procedure. fm : `formula<prop>` The input formula. Returns: `formula<'c> list list` The CNF result of `fn` in a set-of-sets representation. Example `!>"p ==> q" \|> mk_defcnf maincnf` Evaluates to [[`p`; `p_1`]; [`p_1`]; [`p_1`; `~q`]; [`q`; `~p`; `~p_1`]].

Optimized definitional CNF

Functions and values

Function or value	Description
`andcnf (fm, defs, n)` Full Usage: `andcnf (fm, defs, n)` Parameters: fm : `formula<prop>` - The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` - The definitions made so far. n : `bigint` - The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index.	Performs the definitional transformation of the conjuncts. fm : `formula<prop>` The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` The definitions made so far. n : `bigint` The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index.
`defcnf fm` Full Usage: `defcnf fm` Parameters: fm : `formula<prop>` - The input formula. Returns: `formula<prop>` An equisatisfiable CNF of the input formula.	Optimized definitional CNF. It returns an equisatisfiable CNF of the input formula avoiding some redundant definitions. The optimization is obtained, when dealing with an iterated conjunction, by putting the conjuncts in CNF separately and if they in turn are already disjunctions of literals leave them unchanged. fm : `formula<prop>` The input formula. Returns: `formula<prop>` An equisatisfiable CNF of the input formula. Example `!> @"(p \/ (q /\ ~r)) /\ s" \|> defcnf` Evaluates to `(p \/ p_1) /\ (p_1 \/ r \/ ~q) /\ (q \/ ~p_1) /\ s /\ (~p_1 \/ ~r)`.
`defcnfs fm` Full Usage: `defcnfs fm` Parameters: fm : `formula<prop>` - The input formula. Returns: `formula<prop> list list` An equisatisfiable CNF of the input formula in a set-of-sets representation.	Optimized definitional CNF in set-of-sets representation. It returns an equisatisfiable CNF of the input formula in a set-of-sets representation avoiding some redundant definitions. fm : `formula<prop>` The input formula. Returns: `formula<prop> list list` An equisatisfiable CNF of the input formula in a set-of-sets representation. Example `!> @"(p \/ (q /\ ~r)) /\ s" \|> defcnfs` Evaluates to [[`p`; `p_1`]; [`p_1`; `r`; `~q`]; [`q`; `~p_1`]; [`s`]; [`~p_1`; `~r`]].
`orcnf (fm, defs, n)` Full Usage: `orcnf (fm, defs, n)` Parameters: fm : `formula<prop>` - The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` - The definitions made so far. n : `bigint` - The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index.	Performs the definitional transformation of the disjuncts. fm : `formula<prop>` The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` The definitions made so far. n : `bigint` The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint` The triple with the transformed formula, the augmented definitions and a new variable index.
`subcnf sfn op (p, q) (fm, defs, n)` Full Usage: `subcnf sfn op (p, q) (fm, defs, n)` Parameters: sfn : `'a * 'b * 'c -> 'd * 'b * 'c` - The specific definitional CNF procedure. op : `'d -> 'd -> 'e` - The binary formula constructor received from `sfn`. p : `'a` - The left-hand sub-formula. q : `'a` - The right-hand sub-formula. fm : `'f` - The formula to be transformed. defs : `'b` - The definitions made so far. n : `'c` - The current variable index. Returns: `'e * 'b * 'c` The triple with the transformed formula, the augmented definitions and a new variable index.	Links the definitional transformations produced by `sfn` in the different parts of the formula. sfn : `'a * 'b * 'c -> 'd * 'b * 'c` The specific definitional CNF procedure. op : `'d -> 'd -> 'e` The binary formula constructor received from `sfn`. p : `'a` The left-hand sub-formula. q : `'a` The right-hand sub-formula. fm : `'f` The formula to be transformed. defs : `'b` The definitions made so far. n : `'c` The current variable index. Returns: `'e * 'b * 'c` The triple with the transformed formula, the augmented definitions and a new variable index.

3-CNF

Functions and values

Function or value	Description
`andcnf3 (fm, defs, n)` Full Usage: `andcnf3 (fm, defs, n)` Parameters: fm : `formula<prop>` - The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` - The definitions made so far. n : `bigint` - The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint`	Performs the definitional transformation of the conjuncts. It keeps the optimization of putting the conjuncts in CNF separately, but removes the second optimization of leaving unchanged conjuncts that are already a disjunction of literals. In this way guarantees that the result is in 3-CNF. fm : `formula<prop>` The formula to be transformed. defs : `func<formula<prop>, (formula<prop> * formula<prop>)>` The definitions made so far. n : `bigint` The current variable index. Returns: `formula<prop> * func<formula<prop>, (formula<prop> * formula<prop>)> * bigint`
`defcnf3 fm` Full Usage: `defcnf3 fm` Parameters: fm : `formula<prop>` Returns: `formula<prop>`	Optimized definitional CNF that also guarantees 3-CNF in the result. 3-CNF means that each conjunct contains a disjunction of at most three literals. fm : `formula<prop>` Returns: `formula<prop>` Example `!> @"(a \/ b \/ c \/ d) /\ s" \|> defcnf3` Evaluates to `(a \/ p_2 \/ ~p_3) /\ (b \/ p_1 \/ ~p_2) /\ (c \/ d \/ ~p_1) /\ (p_1 \/ ~c) /\ (p_1 \/ ~d) /\ (p_2 \/ ~b) /\ (p_2 \/ ~p_1) /\ p_3 /\ (p_3 \/ ~a) /\ (p_3 \/ ~p_2) /\ s`.