Calculemus

Prop Module

Namespace: Calculemus
Assembly: Calculemus.dll

Basic stuff for propositional logic: datatype, parsing and prettyprinting, syntax and semantics, normal forms.

Note

Although this module defines a specific type prop for primitive propositions, most of the functions defined here for propositional logic are applicable (and intended to be applied) in general to any kind of formula and in particular to our specific type of first order logic formulas fol. These functions handle symbolic computation at the propositional level for any kind of formula unless the signature restricts them to the prop type.

As remarked in the handbook, the defined type prop for propositional variables is fixed here just to make experimentation with some of the operations easier.

Table of contents

Types

Type Description

prop

Type of propositional variables.

Parsing

Functions and values

Function or value Description

!>s

Full Usage: !>s

Parameters:
    s : string - The string to be parsed.

Returns: formula<prop> The parsed prop formula.

A convenient parsing operator to make it easier to parse prop formulas

s : string

The string to be parsed.

Returns: formula<prop>

The parsed prop formula.

Example 

 !> "p /\ q ==> q /\ r"
Evaluates to Imp (And (Atom (P "p"), Atom (P "q")), And (Atom (P "q"), Atom (P "r"))).

parse_prop_formula

Full Usage: parse_prop_formula

Returns: string -> formula<prop>

Parses a string in a propositional formula.

Returns: string -> formula<prop>

parse_propvar vs inp

Full Usage: parse_propvar vs inp

Parameters:
    vs : 'a
    inp : string list

Returns: formula<prop> * string list

Parses atomic propositional variables.

vs : 'a
inp : string list
Returns: formula<prop> * string list

Prettyprinting

Functions and values

Function or value Description

fprint_prop_formula sw

Full Usage: fprint_prop_formula sw

Parameters:
Returns: formula<prop> -> unit

Prints a propositional formula using a TextWriter.

sw : TextWriter
Returns: formula<prop> -> unit

fprint_propvar sw prec p

Full Usage: fprint_propvar sw prec p

Parameters:

Prints a propositional variable using a TextWriter.

sw : TextWriter
prec : 'a
p : prop

print_prop_formula f

Full Usage: print_prop_formula f

Parameters:
Modifiers: inline

Prints a propositional formula.

f : formula<prop>

print_propvar prec p

Full Usage: print_propvar prec p

Parameters:
    prec : 'a
    p : prop

Modifiers: inline
Type parameters: 'a

Prints a propositional variable.

prec : 'a
p : prop

sprint_prop_formula f

Full Usage: sprint_prop_formula f

Parameters:
Returns: string
Modifiers: inline

Returns a string representation of a propositional formula instead of its abstract syntax tree.

f : formula<prop>
Returns: string

sprint_propvar prec p

Full Usage: sprint_propvar prec p

Parameters:
    prec : 'a
    p : prop

Returns: string
Modifiers: inline
Type parameters: 'a

Returns a string representation of a propositional variable.

prec : 'a
p : prop
Returns: string

Syntax operations

Functions and values

Function or value Description

atoms fm

Full Usage: atoms fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: 'a list The set of atoms in the formula

Returns the set of atoms in a formula.

fm : formula<'a>

The input formula.

Returns: 'a list

The set of atoms in the formula

Example 

 !>"p /\ q ==> q /\ r" |> atoms
Evaluates to [P "p"; P "q"; P "r"].

dual fm

Full Usage: dual fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The dual of the input formula.

Returns the dual of the input formula: i.e. the result of systematically exchanging /\ with \/ and also True with False.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The dual of the input formula.

Example 

 !> @"p \/ ~p"
 |> dual
Evaluates to `p /\ ~p`.

pname p

Full Usage: pname p

Parameters:
    p : prop - The input propositional variable.

Returns: string The name of the propositional variable.
Modifiers: inline

Returns the name of a propositional variable.

p : prop

The input propositional variable.

Returns: string

The name of the propositional variable.

Example 

 P "x" |> pname
Evaluates to "x".

psubst subfn fm

Full Usage: psubst subfn fm

Parameters:
    subfn : func<'a, formula<'a>> - The fpf mapping atoms to formulas.
    fm : formula<'a> - The input formula.

Returns: formula<'a> The formula resulting from substituting atoms of fm with the formulas based on the mapping defined in sbfn.

Substitutes atoms in a formula with other formulas based on an fpf.

subfn : func<'a, formula<'a>>

The fpf mapping atoms to formulas.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The formula resulting from substituting atoms of fm with the formulas based on the mapping defined in sbfn.

Example 

 !> "p /\ q /\ p /\ q"
 |> psubst (P"p" |=> !>"p /\ q")
Evaluates to `(p /\ q) /\ q /\ (p /\ q) /\ q`.

Semantics

Functions and values

Function or value Description

eval fm v

Full Usage: eval fm v

Parameters:
    fm : formula<'a> - The input formula.
    v : 'a -> bool - The input valuation.

Returns: bool true, if the formula is true in the give valuation; otherwise false.

Evaluates the truth-value of a formula given a valuation.

A valuation is a function from the set of atoms to the set of truth-values {false, true} (note that these are elements of the metalanguage, in this case F#, that represent the semantic concepts of truth-values and are not the same thing as False and True which are element of the object language and so syntactic elements).

fm : formula<'a>

The input formula.

v : 'a -> bool

The input valuation.

Returns: bool

true, if the formula is true in the give valuation; otherwise false.

Example

The following evaluates the formula given a valuation that evaluates p and r to true and q to false: 

 eval (!>"p /\ q ==> q /\ r") 
     (function P"p" -> true | P"q" -> false | P"r" -> true)
Evaluates to true.

Truth tables

Functions and values

Function or value Description

allvaluations fm

Full Usage: allvaluations fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: ('a -> bool) list All possible valuations of the atoms in the formula.

Returns all possible valuations of the atoms in fm.

This function is not part of the handbook's code and it is added here for convenience and exercise.

fm : formula<'a>

The input formula.

Returns: ('a -> bool) list

All possible valuations of the atoms in the formula.

Example 

 let fm = !> @"(p /\ q) \/ s"
 
 allvaluations fm
 // graphs of all valuations of atoms in fm
 |> List.map (fun v -> 
     atoms fm
     |> List.map (fun a -> (a, v a))
 )
val fm: obj
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val map: mapping: ('T -> 'U) -> list: 'T list -> 'U list
val v: (obj -> obj)
val a: obj
Evaluates to: 
 [[(P "p", false); (P "q", false); (P "s", false)];
  [(P "p", false); (P "q", false); (P "s", true)];
  [(P "p", false); (P "q", true); (P "s", false)];
  [(P "p", false); (P "q", true); (P "s", true)];
  [(P "p", true); (P "q", false); (P "s", false)];
  [(P "p", true); (P "q", false); (P "s", true)];
  [(P "p", true); (P "q", true); (P "s", false)];
  [(P "p", true); (P "q", true); (P "s", true)]]

fprint_truthtable sw fm

Full Usage: fprint_truthtable sw fm

Parameters:

Prints the truth table of the prop formula fm to a TextWriter sw.

See also Prop.print_truthtable

sw : TextWriter

The TextWriter to print to.

fm : formula<prop>

The input prop formula.

Example 

 let file = System.IO.File.CreateText("out.txt")
 fprint_truthtable file (!>"p ==> q")
 file.Close()
val file: System.IO.StreamWriter
namespace System
namespace System.IO
type File = static member AppendAllLines: path: string * contents: IEnumerable<string> -> unit + 1 overload static member AppendAllLinesAsync: path: string * contents: IEnumerable<string> * encoding: Encoding * ?cancellationToken: CancellationToken -> Task + 1 overload static member AppendAllText: path: string * contents: string -> unit + 1 overload static member AppendAllTextAsync: path: string * contents: string * encoding: Encoding * ?cancellationToken: CancellationToken -> Task + 1 overload static member AppendText: path: string -> StreamWriter static member Copy: sourceFileName: string * destFileName: string -> unit + 1 overload static member Create: path: string -> FileStream + 2 overloads static member CreateSymbolicLink: path: string * pathToTarget: string -> FileSystemInfo static member CreateText: path: string -> StreamWriter static member Decrypt: path: string -> unit ...
<summary>Provides static methods for the creation, copying, deletion, moving, and opening of a single file, and aids in the creation of <see cref="T:System.IO.FileStream" /> objects.</summary>
System.IO.File.CreateText(path: string) : System.IO.StreamWriter
System.IO.StreamWriter.Close() : unit
After evaluation the file contains the text 
 p     q     |   formula
 ---------------------
 false false | true  
 false true  | true  
 true  false | false 
 true  true  | true  
 ---------------------

onallvaluations subfn v ats

Full Usage: onallvaluations subfn v ats

Parameters:
    subfn : ('a -> bool) -> bool - A function that given a valuation return true or false.
    v : 'a -> bool - The default valuation for other atoms.
    ats : 'a list - The list of atoms on which to test all possibile valuations.

Returns: bool true, if subfn returns true on all possible valuations of the atoms ats with valuation v for all other atoms; otherwise false.

Tests whether a function subfn returns true on all possible valuations of the atoms ats, using an existing valuation v for all other atoms.

This function is used to define both truth-table (see Prop.print_truthtable) and Prop.tautology

subfn : ('a -> bool) -> bool

A function that given a valuation return true or false.

v : 'a -> bool

The default valuation for other atoms.

ats : 'a list

The list of atoms on which to test all possibile valuations.

Returns: bool

true, if subfn returns true on all possible valuations of the atoms ats with valuation v for all other atoms; otherwise false.

Example

eval True returns true on all valuations: 

 onallvaluations (eval True) (fun _ -> false) []
Evaluates to true.

print_truthtable fm

Full Usage: print_truthtable fm

Parameters:
Modifiers: inline

Prints the truth table of the prop formula fm to the stdout.

Each logical connective is interpreted by a corresponding bool operator of the metalanguage.

A truth-table shows how the truth-value assigned to a formula is determined by those of its atoms, based on the interpretation of its logical connectives.

For binary connective we have: \begin{array}{|c|c||c|c|c|c|} \hline p & q & p \land q & p \lor q & p \Rightarrow q & p \Leftrightarrow q \\ \hline false & false & false & false & true & true \\ \hline false & true & false & true & true & false \\ \hline true & false & false & true & false & false \\ \hline true & true & true & true & true & true \\ \hline \end{array} while for the unary negation: \begin{array}{|c||c|} \hline p & \neg p \\ \hline false & true\\ \hline true & false\\ \hline \end{array}

A truth table has one column for each propositional variable and one final column showing all of the possible results of the logical operation that the table represents. Each row of the truth table contains one possible configuration of the propositional variables, and the result of the operation for those values.

In particular, truth-tables can be used to show whether (i) a prop formula is logically valid (i.e. a tautology: see Prop.tautology that, as this function, is based on Prop.onallvaluations) when the result column has true in each rows of the table; (ii) Prop.satisfiable, when the result colum has true at least in one row; (iii) Prop.unsatisfiable when has false in each rows.

fm : formula<prop>

The input prop formula.

Example 
 print_truthtable !>"p /\ q ==> q /\ r"
After evaluation the following text is printed to the stdout: 
 p     q     r     |   formula
 ---------------------------
 false false false | true  
 false false true  | true  
 false true  false | true  
 false true  true  | true  
 true  false false | true  
 true  false true  | true  
 true  true  false | false 
 true  true  true  | true  
 ---------------------------

sprint_truthtable fm

Full Usage: sprint_truthtable fm

Parameters:
Returns: string The string representation of the truth table of the formula.
Modifiers: inline

Returns a string representation of the truth table of the prop formula fm.

See also Prop.print_truthtable

fm : formula<prop>

The input prop formula.

Returns: string

The string representation of the truth table of the formula.

Example 

 sprint_truthtable !>"p ==> q"
Evaluates to: 
 "p     q     |   formula
 ---------------------
 false false | true  
 false true  | true  
 true  false | false 
 true  true  | true  
 ---------------------
 
 "

Tautology, unsatisfiability and satisfiability

Functions and values

Function or value Description

satisfiable fm

Full Usage: satisfiable fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: bool true, if the formula is a satisfiable at the propositional level; otherwise false.

Checks if a formula is satisfiable at the propositional level.

fm : formula<'a>

The input formula.

Returns: bool

true, if the formula is a satisfiable at the propositional level; otherwise false.

Example 

 !> "p /\ ~p"
 |> satisfiable
Evaluates to false.

Example 

 !> @"p"
 |> satisfiable
Evaluates to true.

tautology fm

Full Usage: tautology fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: bool true, if the formula is a tautology at the propositional level; otherwise false.

Checks if a formula is a tautology at the propositional level.

fm : formula<'a>

The input formula.

Returns: bool

true, if the formula is a tautology at the propositional level; otherwise false.

Example 

 !> @"p \/ ~p"
 |> tautology
Evaluates to true.

Example 

 !> @"p \/ q ==> p"
 |> tautology
Evaluates to false.

Example 

 !> @"p \/ q ==> q \/ (p <=> q)"
 |> tautology
Evaluates to false.

Example 

 !> @"(p \/ q) /\ ~(p /\ q) ==> (~p <=> q)"
 |> tautology
Evaluates to false.

unsatisfiable fm

Full Usage: unsatisfiable fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: bool true, if the formula is a unsatisfiable at the propositional level; otherwise false.

Checks if a formula is unsatisfiable at the propositional level.

fm : formula<'a>

The input formula.

Returns: bool

true, if the formula is a unsatisfiable at the propositional level; otherwise false.

Example 

 !> "p /\ ~p"
 |> unsatisfiable
Evaluates to true.

Example 

 !> @"p"
 |> unsatisfiable
Evaluates to false.

Simplification

Functions and values

Function or value Description

psimplify fm

Full Usage: psimplify fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The formula simplified.

Performs a propositional simplification routine eliminating the basic propositional constants False and True and the double negations ~~p.

Completes the simplification routine psimplify1 applying it at every level of the formula.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The formula simplified.

Example 

 !> "((x ==> y) ==> true) \/ ~false"
 |> psimplify
Evaluates to `true`.

psimplify1 fm

Full Usage: psimplify1 fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The formula simplified.

Performs a propositional simplification routine (but just at the first level) of the input formula, eliminating the basic propositional constants False and True and the double negations ~~p.

This function applies to formulas a simplification routine similar to the one Intro.simplify1 applies on algebraic expressions. It eliminates the basic propositional constants \(\bot\) and \(\top\) based on the equivalences similar to the following (see the implementation for details):

  • \(\bot \land p \Leftrightarrow \bot\)
  • \(\top \lor p \Leftrightarrow p\)
  • \(p \Rightarrow \bot \Leftrightarrow \neg p\)
  • ...
At the same time, it also eliminates double negations \(\neg \neg p\).

fm : formula<'a>

The input formula.

Returns: formula<'a>

The formula simplified.

Example 

 !> "false /\ p"
 |> psimplify1
Evaluates to `false`.

Literals

Functions and values

Function or value Description

negate lit

Full Usage: negate lit

Parameters:
    lit : formula<'a> - The input literal.

Returns: formula<'a> The negated literal if the input is positive and vice versa.

Changes a literal into its contrary.

A literal is an atomic formula or its negation. This function can be applied to any kind of formulas but is specifically intended to be used on literals.

lit : formula<'a>

The input literal.

Returns: formula<'a>

The negated literal if the input is positive and vice versa.

Example 

 !> "p" |> negate
Evaluates to `~p`.

Example 

 !> "~p" |> negate
Evaluates to `p`.

negative lit

Full Usage: negative lit

Parameters:
    lit : formula<'a> - The input literal.

Returns: bool true, if the literal is negative; otherwise false.

Checks if a literal is negative.

A literal is an atomic formula or its negation. This function can be applied to any kind of formulas but is specifically intended to be used on literals.

lit : formula<'a>

The input literal.

Returns: bool

true, if the literal is negative; otherwise false.

Example 

 !> "~p" |> negative
Evaluates to true.

Example 

 !> "p" |> negative
Evaluates to false.

positive lit

Full Usage: positive lit

Parameters:
    lit : formula<'a> - The input literal.

Returns: bool true, if the literal is positive; otherwise false.

Checks if a literal is positive.

A literal is an atomic formula or its negation. This function can be applied to any kind of formulas but is specifically intended to be used on literals.

lit : formula<'a>

The input literal.

Returns: bool

true, if the literal is positive; otherwise false.

Example 

 !> "p" |> positive
Evaluates to true.

Example 

 !> "~p" |> positive
Evaluates to false.

Negation Normal Form

Functions and values

Function or value Description

nenf fm

Full Usage: nenf fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The input formula transformed in a negation normal form that keeps equivalences.

Changes a formula into negation normal form but keeps logical equivalences.

Applies Prop.psimplify first and then Prop.nenf_naive.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The input formula transformed in a negation normal form that keeps equivalences.

Example 

 !> "~ (p <=> q)"
 |> nenf
Evaluates to `p <=> ~q)`.

Example 

 !> "~ (false <=> q)"
 |> nenf
Evaluates to `q`.

nenf_naive fm

Full Usage: nenf_naive fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The input formula transformed in a negation normal form that keeps equivalences and logical constants mixed with other formulas.

Changes a formula into negation normal form but keeps logical equivalences and False and True mixed with other formulas.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The input formula transformed in a negation normal form that keeps equivalences and logical constants mixed with other formulas.

Example 

 !> "~ (p <=> q)"
 |> nenf_naive
Evaluates to `p <=> ~q`.

Example 

 !> "~ (false <=> q)"
 |> nenf_naive
Evaluates to `false <=> ~q`.

nnf fm

Full Usage: nnf fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The input formula transformed in a negation normal form.

Changes a formula into a naive negation normal form.

A formula is in negation normal form (NNF) if it is constructed from literals using only the binary connectives \(\land\) and \(\lor\), or else is one of the degenerate cases \(\top\) and \(\bot\).

It is analogous to the following procedure in ordinary algebra: (i) replace subtraction by its definition \(x - y = x + -y\) and then (ii) systematically push negations down using \(-(x + y) = -x + -y\), \(-(xy) = (-x)y\), \(-(-x) = x\).

nnf implements a complete transformation in NNF applying Prop.psimplify first and then Prop.nnf_naive.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The input formula transformed in a negation normal form.

Note

Negation normal form is not a canonical form: for example, \(a \land (b \lor \lnot c)\) and \((a \land b) \lor (a \land \lnot c)\) are equivalent, and are both in negation normal form. (from https://en.wikipedia.org/wiki/Negation_normal_form)

Example 

 !> "~ (p ==> false)"
 |> nnf
Evaluates to `p`.

Example 

 !> "(p <=> q) <=> ~(r ==> s)"
 |> nnf
Evaluates to `(p /\ q \/ ~p /\ ~q) /\ r /\ ~s \/ (p /\ ~q \/ ~p /\ q) /\ (~r \/ s)`.

nnf_naive fm

Full Usage: nnf_naive fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The input formula transformed in a naive negation normal form.

Changes a formula into a naive negation normal form.

A formula is in negation normal form (NNF) if it is constructed from literals using only the binary connectives \(\land\) and \(\lor\), or else is one of the degenerate cases \(\top\) and \(\bot\). nnf_naive implements an incomplete transformation of NNF which pushes down negation on atoms and removes the binary connective \(\Rightarrow\) and \(\Leftrightarrow\) but keeps \(\top\) and \(\bot\) mixed with other formulas.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The input formula transformed in a naive negation normal form.

Example 

 !> "~ (p ==> false)"
 |> nnf_naive
Evaluates to `p /\ ~false`.

Disjunctive Normal Form

Functions and values

Function or value Description

allsatvaluations subfn v pvs

Full Usage: allsatvaluations subfn v pvs

Parameters:
    subfn : ('a -> bool) -> bool - A function that given a valuation return true or false.
    v : 'a -> bool - The default valuation for other atoms.
    pvs : 'a list - The list of atoms on which to test all possibile valuations.

Returns: ('a -> bool) list The list of valuations for which subfn holds on pvs.

A close analogue of Prop.onallvaluations that collects into a list the valuations for which subfn holds.

subfn : ('a -> bool) -> bool

A function that given a valuation return true or false.

v : 'a -> bool

The default valuation for other atoms.

pvs : 'a list

The list of atoms on which to test all possibile valuations.

Returns: ('a -> bool) list

The list of valuations for which subfn holds on pvs.

Example 

 let fm = !> "p /\ q"
 let atms = atoms fm
 let satvals = allsatvaluations (eval fm) (fun _ -> false) atms
 
 satvals[0] (P"p") // true
 satvals[0] (P"q") // true
 satvals[0] (P"x") // false
val fm: obj
val atms: obj
val satvals: (int list -> obj -> obj)

Example

allsatvaluations applied to eval fm extracts all valuations satisfying fm. 

 let fm = !> @"(p /\ q) \/ (s /\ t)"
 let atms = atoms fm
 
 allsatvaluations (eval fm) (fun _ -> false) atms
 // graphs of all valuations satisfying fm
 |> List.map (fun v -> 
     atms
     |> List.map (fun a -> (a, v a))
 )
val fm: obj
val atms: obj list
Multiple items
module List from Microsoft.FSharp.Collections

--------------------
type List<'T> = | op_Nil | op_ColonColon of Head: 'T * Tail: 'T list interface IReadOnlyList<'T> interface IReadOnlyCollection<'T> interface IEnumerable interface IEnumerable<'T> member GetReverseIndex: rank: int * offset: int -> int member GetSlice: startIndex: int option * endIndex: int option -> 'T list static member Cons: head: 'T * tail: 'T list -> 'T list member Head: 'T member IsEmpty: bool member Item: index: int -> 'T with get ...
val map: mapping: ('T -> 'U) -> list: 'T list -> 'U list
val v: (obj -> obj)
val a: obj
Evaluates to: 
 [[(P "p", false); (P "q", false); (P "s", true); (P "t", true)];
  [(P "p", false); (P "q", true); (P "s", true); (P "t", true)];
  [(P "p", true); (P "q", false); (P "s", true); (P "t", true)];
  [(P "p", true); (P "q", true); (P "s", false); (P "t", false)];
  [(P "p", true); (P "q", true); (P "s", false); (P "t", true)];
  [(P "p", true); (P "q", true); (P "s", true); (P "t", false)];
  [(P "p", true); (P "q", true); (P "s", true); (P "t", true)]]

distrib s1 s2

Full Usage: distrib s1 s2

Parameters:
    s1 : 'a list list - The first input set of set.
    s2 : 'a list list - The second input set of set.

Returns: 'a list list The set of the unions of first sets with the latter.

Takes two sets of sets and returns the set of the unions of each set in the first with sets in the second.

It is used to obtain the distributive laws of /\ and \/ (see Prop.distrib_naive) in the context of a set of sets representation of dnf (see Prop.purednf)

s1 : 'a list list

The first input set of set.

s2 : 'a list list

The second input set of set.

Returns: 'a list list

The set of the unions of first sets with the latter.

Example 

 distrib [[1;2];[2]] [[3];[4]]
Evaluates to [[1; 2; 3]; [1; 2; 4]; [2; 3]; [2; 4]].

Example

Representing the distributive laws: 

 distrib [["p"]] [["q"];["r"]] // [["p"; "q"]; ["p"; "r"]]
 distrib [["p"];["q"]] [["r"]] // [["p"; "r"]; ["q"; "r"]]

distrib_naive fm

Full Usage: distrib_naive fm

Parameters:
    fm : formula<'a> - The input formula with immediate subformulas in DNF.

Returns: formula<'a> The formula transformed with the distributive laws of /\ and \/, if its immediate subformulas are in DNF; otherwise, the input unchanged.

Applies the distributive laws of /\ and \/ to the input formula fm, assuming that its immediate subformulas are in DNF.

The distributive laws are the following:

  • p /\ (q \/ r) <=> p /\ q \/ p /\ r
  • (p \/ q) /\ r <=> p /\ r \/ q /\ r.
Analogous to the following in algebra:
  • x(y + z) = xy + xz
  • (x + y)z = xz + yz.

fm : formula<'a>

The input formula with immediate subformulas in DNF.

Returns: formula<'a>

The formula transformed with the distributive laws of /\ and \/, if its immediate subformulas are in DNF; otherwise, the input unchanged.

Example 

 !> @"p /\ (q \/ r)" |> distrib_naive
Evaluates to `p /\ q \/ p /\ r`.

Example 

 !> "p ==> q" |> distrib_naive
Evaluates to `p ==> q`.

dnf fm

Full Usage: dnf fm

Parameters:
    fm : formula<'a> - The input formulas.

Returns: formula<'a> A dnf equivalent of the input.

Transforms any kind of formula in disjunctive normal form.

A formula is in disjunctive normal form (DNF) if it is an iterated disjunction of conjunctions of litterals.

It is analogous to a fully expanded sum of products expression like \(x^3 + x^2 y + xy + z\) in algebra.

It is not canonical since for example p /\ ~q /\ r \/ p /\ q /\ ~r \/ p /\ q /\ r and p /\ q \/ p /\ r are both equivalent DNF.

fm : formula<'a>

The input formulas.

Returns: formula<'a>

A dnf equivalent of the input.

Example 

 !> @"p ==> q" |> dnf
Evaluates to `q \/ ~p`.

Example 

 let fm = !> @"(p \/ q /\ r) /\ (~p \/ ~r)"
 let dnf = dnf fm // `p /\ ~r \/ q /\ r /\ ~p`
 tautology(mk_iff fm dnf)
val fm: obj
val dnf: obj
Evaluates to true.

dnf_by_truth_tables fm

Full Usage: dnf_by_truth_tables fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The input formula transformed in disjunctive normal form.

Transforms a formula fm in disjunctive normal form by the valuations satisfying it.

See Prop.dnf for a definition of DNF.

dnf_by_truth_tables, from all valuations satisfying the formula, generates an equivalent that is the disjunction of the conjunctions of the atoms that in each evaluation are mapped to true or their negations if they're mapped to false. Thus, it is based on the same semantic process of truth-tables.

Note also that since it is based on truth-tables (or more precisely on valuations), it generates disjunctions in which each conjunct contains every atoms of the original formula, while other dnf functions generate more cleaner results.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The input formula transformed in disjunctive normal form.

Example 

 !> @"p ==> q"
 |> dnf_by_truth_tables 
 // Evaluates to `~p /\ ~q \/ ~p /\ q \/ p /\ q`
 
 // Note the symmetry between the conjunctions 
 // and the true-rows of the truth table.
 !> @"p ==> q"
 |> print_truthtable
 
 // p     q     |   formula
 // ---------------------
 // false false | true  
 // false true  | true  
 // true  false | false 
 // true  true  | true  
 // ---------------------

list_conj l

Full Usage: list_conj l

Parameters:
    l : formula<'a> list - The list of formulas to conjunct.

Returns: formula<'a> The conjunction of the input formulas.

Constructs a conjunction from a list of formulas.

l : formula<'a> list

The list of formulas to conjunct.

Returns: formula<'a>

The conjunction of the input formulas.

Example 

 list_conj [!>"p";!>"q";!>"r"]
Evaluates to `p /\ q /\ r`.

list_disj l

Full Usage: list_disj l

Parameters:
    l : formula<'a> list - The list of formulas to disjunct.

Returns: formula<'a> The disjunction of the input formulas.

Constructs a disjunction from a list of formulas.

l : formula<'a> list

The list of formulas to disjunct.

Returns: formula<'a>

The disjunction of the input formulas.

Example 

 list_disj [!>"p";!>"q";!>"r"]
Evaluates to `p \/ q \/ r`.

mk_lits pvs v

Full Usage: mk_lits pvs v

Parameters:
    pvs : formula<'a> list - The input list of formulas.
    v : 'a -> bool - The input valuation.

Returns: formula<'a> The conjunction of the pvs formulas (positive or negated depending on v).

Constructs a conjunction from a list of formulas pvs and their negations, according to whether each is satisfied by a valuation v.

As the name suggest, it is intended to be used on literals and actually is used just to define Prop.dnf_by_truth_tables

pvs : formula<'a> list

The input list of formulas.

v : 'a -> bool

The input valuation.

Returns: formula<'a>

The conjunction of the pvs formulas (positive or negated depending on v).

Example 

 mk_lits [!>"p";!>"q"] 
     (function P"p" -> true | P"q" -> false)
Evaluates to `p /\ ~q`.

purednf fm

Full Usage: purednf fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> list list A dnf equivalent of the input formula in a set of sets representation with possible superfluous and subsumed disjuncts, if the input is in NNF; otherwise a meaningless list of lists of the input itself.

Transform a formula already in NNF in DNF with a set of sets representation form as output (with possible superfluous and subsumed disjuncts in the result).

The resulting global set represents the disjunction and the subsets the conjunctions: e.g. the set of sets representation of p /\ q \/ ~ p /\ r is [[p; q]; [~ p; r]].

fm : formula<'a>

The input formula.

Returns: formula<'a> list list

A dnf equivalent of the input formula in a set of sets representation with possible superfluous and subsumed disjuncts, if the input is in NNF; otherwise a meaningless list of lists of the input itself.

Example 

 !> @"(p \/ q /\ r) /\ (~p \/ ~r)"
 |> purednf
Evaluates to [[`p`; `~p`]; [`p`; `~r`]; [`q`; `r`; `~p`]; [`q`; `r`; `~r`]].

Example 

 !> "p ==> q"
 |> purednf
Evaluates to [[`p ==> q`]].

rawdnf fm

Full Usage: rawdnf fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> The formula transformed in a raw DNF if the input is already in NNF; otherwise, the input unchanged.

Transforms an NNF formula in a raw disjunctive normal form.

It is raw because:

  1. it requires the input formula being in NNF;
  2. it's hard to read due to mixed associations in iterated conjunctions and disjunctions enclosed in parentheses. E.g. (p /\ q \/ p /\ r) \/ s instead of p /\ q \/ p /\ r \/ s;
  3. it can contain redundant disjuncts equivalent to False.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The formula transformed in a raw DNF if the input is already in NNF; otherwise, the input unchanged.

Example 

 !> @"p /\ (q \/ r) \/ s" |> rawdnf
Evaluates to `(p /\ q \/ p /\ r) \/ s`.

Example 

 !> "p ==> q" |> rawdnf
Evaluates to `p ==> q`.

Example 

 !> "(p \/ q /\ r) /\ (~p \/ ~r)" |> rawdnf
Evaluates to `(p /\ ~p \/ (q /\ r) /\ ~p) \/ p /\ ~r \/ (q /\ r) /\ ~r`.

simpdnf fm

Full Usage: simpdnf fm

Parameters:
    fm : formula<'a> - The input formulas.

Returns: formula<'a> list list A set of set representation of a dnf equivalent of the input.

Transforms any kind of formula in disjunctive normal form returning a set of set representation.

It exploits the list of list representation filtering out trivial complementary literals and subsumed ones (with subsumption checking, done very naively: quadratic).

fm : formula<'a>

The input formulas.

Returns: formula<'a> list list

A set of set representation of a dnf equivalent of the input.

Example 

 !> @"p ==> q" |> simpdnf
Evaluates to [[`q`]; [`~p`]].

trivial lits

Full Usage: trivial lits

Parameters:
    lits : formula<'a> list - The input list of literals.

Returns: bool true, if there are complementary literals in the input list; otherwise false.

Check if there are complementary literals of the form p and ~ p in a list of formulas.

lits : formula<'a> list

The input list of literals.

Returns: bool

true, if there are complementary literals in the input list; otherwise false.

Example 

 trivial [!>"p";!>"~p"]
Evaluates to true.

Example 

 trivial [!>"p";!>"~q"]
Evaluates to false.

Conjunctive Normal Form

Functions and values

Function or value Description

cnf fm

Full Usage: cnf fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> A cnf equivalent of the input formula.

Transforms any kind of input formulas in conjunctive normal.

A formula is in conjunctive normal form (CNF) if it is an iterated conjunction of disjunctions of litterals.

It is analogous to a fully factorized product of sums expression like \((x + 1)(y + 2)(z + 3)\) in algebra.

fm : formula<'a>

The input formula.

Returns: formula<'a>

A cnf equivalent of the input formula.

Example 

 let fm = !> @"(p \/ q /\ r) /\ (~p \/ ~r)"
 let cnf = cnf fm // `(p \/ q) /\ (p \/ r) /\ (~p \/ ~r)`
 tautology(mk_iff fm cnf)
val fm: obj
val cnf: obj
Evaluates to true.

purecnf fm

Full Usage: purecnf fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> list list A cnf equivalent of the input formula in a set of sets representation with possible superfluous and subsumed conjuncts.

Transforms any kind of input formulas in conjunctive normal form with a set of sets representation form as output, but keeps possible superfluous and subsumed conjuncts.

In the cnf context the outer set represents the iterated conjunction and the subsets the disjunctions. Thus, [[p; q]; [~ p; r]] represents p \/ q /\ ~ p \/ r

fm : formula<'a>

The input formula.

Returns: formula<'a> list list

A cnf equivalent of the input formula in a set of sets representation with possible superfluous and subsumed conjuncts.

Example 

 !> @"p ==> q" |> purecnf
Evaluates to [[`q`; `~p`]].

Example 

 !> @"p \/ ~p" |> purecnf
Evaluates to [[`p`; `~p`]].

simpcnf fm

Full Usage: simpcnf fm

Parameters:
    fm : formula<'a> - The input formula.

Returns: formula<'a> list list A cnf equivalent of the input formula in a set of sets representation.

Transforms any kind of input formulas in conjunctive normal form with a set of sets representation form as output.

It exploits the list of list representation filtering out trivial complementary literals and subsumed ones.

fm : formula<'a>

The input formula.

Returns: formula<'a> list list

A cnf equivalent of the input formula in a set of sets representation.

Example 

 !> @"p ==> q" |> simpcnf
Evaluates to [[`q`; `~p`]].

Example 

 !> @"p \/ ~p" |> simpcnf
Evaluates to [[`p`; `~p`]].