Calculemus

Skolem Module

Namespace: Calculemus
Assembly: Calculemus.dll

Prenex and Skolem normal forms.

Table of contents

Simplification

Functions and values

Function or value Description

simplify fm

Full Usage: simplify fm

Parameters:
Returns: formula<fol> The simplified formula.

Simplification routine.

It performs a simplification eliminating the basic propositional constants False and True and also the vacuous quantifiers (those applied to variables that do not occur free in the body).

It applies Skolem.simplify1 repeatedly at every level of the formula in a recursive bottom-up sweep.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The simplified formula.

Example 

 simplify !!"true ==> (p <=> (p <=>false))"
Evaluates to `p <=> ~p>`.

Example 

 simplify !!"exists x y z. P(x) ==> Q(z) ==> false"
Evaluates to `exists x z. P(x) ==> ~Q(z)`.

simplify1 fm

Full Usage: simplify1 fm

Parameters:
Returns: formula<fol> The simplified formula.

First level simplification routine.

It performs a simplification routine but just at the first level of the input formula fm. It eliminates the basic propositional constants False and True and also the vacuous universal and existential quantifiers (those applied to variables that does not occur free in the body).

fm : formula<fol>

The input formula.

Returns: formula<fol>

The simplified formula.

Example 

 simplify1 !!"exists x. P(y)"
Evaluates to `P(y)`.

Example 

 simplify1 !!"true ==> exists x. P(x)"
Evaluates to `exists x. P(x)`.

Negation normal form

Functions and values

Function or value Description

nnf fm

Full Usage: nnf fm

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

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

Transforms the input formula fm in first order negation normal form.

It eliminates implication and equivalence, and pushes down negations through quantifiers.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The formula in negation normal form.

Note

Pay attention that in Prop there is a propositional version of Prop.nnf. If all modules have been opened, qualify the exact version to be used.

Example 

 nnf !!"~ exists x. P(x) <=> Q(x)"
Evaluates to `forall x. P(x) /\ ~Q(x) \/ ~P(x) /\ Q(x)`.

Prenex normal form

Functions and values

Function or value Description

pnf fm

Full Usage: pnf fm

Parameters:
Returns: formula<fol> The prenex normal form equivalent of the input formula.

Transforms the input formula fm in prenex normal form and simplifies it.

  • simplifies away False, True, vacuous quantification, etc.;
  • eliminates implication and equivalence, pushes down negations;
  • pulls out quantifiers.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The prenex normal form equivalent of the input formula.

Example 

 pnf !! @"(forall x. P(x) \/ R(y)) ==> exists y z. Q(y) \/ ~(exists z. P
 (z) /\ Q(z))"
Evaluates to `exists x. forall z. ~P(x) /\ ~R(y) \/ Q(x) \/ ~P(z) \/ ~Q(z)`.

prenex fm

Full Usage: prenex fm

Parameters:
Returns: formula<fol> The equivalent of the input (already simplified and in nnf) with quantifiers pulled out.

It pulls out quantifiers of a formula supposed to be already simplified and in nnf.

It deals with the subformulas of quantified formulas, and for the others (conjunctions and disjunctions) calls Skolem.pullquants.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The equivalent of the input (already simplified and in nnf) with quantifiers pulled out.

Example 

 !!"forall x. P(X) /\ forall y. Q(x,y)"
 |> prenex
Evaluates to `forall x y. P(X) /\ Q(x,y)`.

pullq (l, r) fm quant op x y p q

Full Usage: pullq (l, r) fm quant op x y p q

Parameters:
    l : bool - The flag to indicate if the left hand formula should be changed.
    r : bool - The flag to indicate if the right hand formula should be changed.
    fm : formula<fol> - The input formula.
    quant : string -> formula<fol> -> formula<fol> - The quantification constructor to apply.
    op : formula<fol> -> formula<fol> -> formula<fol> - The binary connective constructor to apply.
    x : string - The variable to check in the left hand formula to prevent it from being bound.
    y : string - The variable to check in the right hand formula to prevent it from being bound.
    p : formula<fol> - The left hand formula.
    q : formula<fol> - The right hand formula.

Returns: formula<fol> The formula with the quantifiers pulled out.

Auxiliary function to define Skolem.pullquants.

It deals with various similar subcases and calls the main Skolem.pullquants function again on the body to pull up further quantifiers.

l : bool

The flag to indicate if the left hand formula should be changed.

r : bool

The flag to indicate if the right hand formula should be changed.

fm : formula<fol>

The input formula.

quant : string -> formula<fol> -> formula<fol>

The quantification constructor to apply.

op : formula<fol> -> formula<fol> -> formula<fol>

The binary connective constructor to apply.

x : string

The variable to check in the left hand formula to prevent it from being bound.

y : string

The variable to check in the right hand formula to prevent it from being bound.

p : formula<fol>

The left hand formula.

q : formula<fol>

The right hand formula.

Returns: formula<fol>

The formula with the quantifiers pulled out.

Example 

 let fm = !!"P(x) /\ exists y. Q(y)"
 pullq (false, true) fm mk_exists mk_and "y" "y" !!"P(x)" !!"Q(y)"
val fm: obj
Evaluates to `forall x. exists y. P(x) /\ P(y)`.

pullquants fm

Full Usage: pullquants fm

Parameters:
Returns: formula<fol> The formula with the quantifiers pulled out.

It pulls out quantifiers of top level conjunctions or disjunctions.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The formula with the quantifiers pulled out.

Example 

 !!"(forall x. P(x)) /\ (exists y. P(y))"
 |> pullquants
Evaluates to `forall x. exists y. P(x) /\ P(y)`.

Get functions in term and formula

Functions and values

Function or value Description

funcs tm

Full Usage: funcs tm

Parameters:
    tm : term - The input term.

Returns: (string * int) list The list of name-arity pairs of the functions in the term.

Returns the functions present in the input term tm.

tm : term

The input term.

Returns: (string * int) list

The list of name-arity pairs of the functions in the term.

Example 

 funcs !!!"x + 1"
Evaluates to [("+", 2); ("1", 0)].

functions fm

Full Usage: functions fm

Parameters:
Returns: (string * int) list The list of name-arity pairs of the functions in the formula.

Returns the functions present in the input formula fm.

fm : formula<fol>

The input formula.

Returns: (string * int) list

The list of name-arity pairs of the functions in the formula.

Example 

 functions !!"x + 1 > 0 /\ f(z) > g(z,i)"
Evaluates to [("+", 2); ("0", 0); ("1", 0); ("f", 1); ("g", 2)].

Core Skolemization

Functions and values

Function or value Description

skolem fm fns

Full Usage: skolem fm fns

Parameters:
    fm : formula<fol> - The input formula.
    fns : string list - The list of strings to avoid as names of the Skolem functions.

Returns: formula<fol> * string list The pair of the Skolemized formula together with the updated list of strings to avoid as names of the Skolem functions.

Core Skolemization function specifically intended to be used on formulas already simplified and in nnf.

It simply recursively descends the formula, Skolemizing any existential formulas and then proceeding to subformulas using skolem2 for binary connectives.

fm : formula<fol>

The input formula.

fns : string list

The list of strings to avoid as names of the Skolem functions.

Returns: formula<fol> * string list

The pair of the Skolemized formula together with the updated list of strings to avoid as names of the Skolem functions.

Example 

 skolem !!"forall x. exists y. P(x,y)" []
Evaluates to (`forall x. P(x,f_y(x))`, ["f_y"]).

skolem2 cons (p, q) fns

Full Usage: skolem2 cons (p, q) fns

Parameters:
    cons : formula<fol> * formula<fol> -> formula<fol> - The binary connective constructor to apply.
    p : formula<fol> - The left hand formula.
    q : formula<fol> - The right hand formula.
    fns : string list - The list of strings to avoid as names of the Skolem functions.

Returns: formula<fol> * string list The pair of the Skolemized and reconstructed binary formula together with the updated list of strings to avoid as names of the Skolem functions.

Auxiliary to Skolem.skolem when dealing with binary connectives.

It updates the set of functions to avoid with new Skolem functions introduced into one formula before tackling the other.

cons : formula<fol> * formula<fol> -> formula<fol>

The binary connective constructor to apply.

p : formula<fol>

The left hand formula.

q : formula<fol>

The right hand formula.

fns : string list

The list of strings to avoid as names of the Skolem functions.

Returns: formula<fol> * string list

The pair of the Skolemized and reconstructed binary formula together with the updated list of strings to avoid as names of the Skolem functions.

Example 

 let p,q = !!"forall x. exists y. P(x,y)", !!"forall x. exists y. Q(x,y)"
 skolem2 And (p,q) []
val p: obj
val q: obj
Evaluates to (`(forall x. P(x,f_y(x))) /\ (forall x. Q(x,f_y'(x)))`, ["f_y'"; "f_y"]).

Overall Skolemization

Functions and values

Function or value Description

askolemize fm

Full Usage: askolemize fm

Parameters:
Returns: formula<fol> The input formula with all existential quantifiers replaced by Skolem functions.

Skolemizes, simplifies and puts in NNF the input formula fm.

fm : formula<fol>

The input formula.

Returns: formula<fol>

The input formula with all existential quantifiers replaced by Skolem functions.

Note

See also: Skolem.nnf, Skolem.simplify

Example 

 askolemize !!"forall x. exists y. R(x,y)"
Evaluates to `forall x. R(x,f_y(x))`.

skolemize fm

Full Usage: skolemize fm

Parameters:
Returns: formula<fol> An equisatisfiable Skolem normal form of the input with also the universal quantifiers removed.

Puts the input formula fm into Skolem normal form while also removing all universal quantifiers.

It puts the formula in prenex normal form, substitutes existential quantifiers with Skolem functions and also removes all universal quantifiers.

fm : formula<fol>

The input formula.

Returns: formula<fol>

An equisatisfiable Skolem normal form of the input with also the universal quantifiers removed.

Example 

 skolemize !!"forall x. exists y. R(x,y)"
Evaluates to `R(x,f_y(x))`.

specialize fm

Full Usage: specialize fm

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

Returns: formula<'a> The input formula with all universal quantifiers removed.

Removes all universal quantifiers from the input formula fm.

fm : formula<'a>

The input formula.

Returns: formula<'a>

The input formula with all universal quantifiers removed.

Example 

 specialize !!"forall x y. P(x) /\ P(y)"
Evaluates to `P(x) /\ P(y)`.