Calculemus

Herbrand Module

Namespace: Calculemus
Assembly: Calculemus.dll

Relation between first order and propositional logic; Herbrand theorem.

Table of contents

Propositional valuation

Functions and values

Function or value Description

pholds d fm

Full Usage: pholds d fm

Parameters:
    d : formula<'a> -> bool - The propositional valuation that maps atomic formulas to truth values.
    fm : formula<'a> - The input formula.

Returns: bool

Evaluates the truth-value of a quantifier-free formula, in the sense of propositional logic, given a valuation of its atoms.

It is a variant of the notion of propositional evaluation Prop.eval where the input propositional valuation d maps atomic formulas themselves to truth values.

d : formula<'a> -> bool

The propositional valuation that maps atomic formulas to truth values.

fm : formula<'a>

The input formula.

Returns: bool
Exception Thrown with message Not part of propositional logic. when the input formula contains quantifiers.
Example 

 !!"P(x) /\ Q(x)"
 |> pholds (function 
     | x when x = !!"P(x)" -> true 
     | x when x = !!"Q(x)" -> true 
     | _ -> false
 )
Evaluates to true.

Example 

 !!"P(x) /\ Q(x)"
 |> pholds (function 
     | x when x = !!"P(x)" -> true 
     | x when x = !!"Q(x)" -> false 
     | _ -> false
 )
Evaluates to false.

Example 

 !!"forall x. P(x) /\ Q(x)"
 |> pholds (function 
     | x when x = !!"P(x)" -> true
     | x when x = !!"Q(x)" -> true
     | _ -> false
 )
Throws System.Exception: Not part of propositional logic..

Herbrand models

Functions and values

Function or value Description

groundterms cntms funcs n

Full Usage: groundterms cntms funcs n

Parameters:
    cntms : term list - The input list of constant terms.
    funcs : (string * int) list - The input list of function name-arity pairs.
    n : int - The number of function symbols the resulting ground terms will contain.

Returns: term list The input cntms itself, if n is 0; otherwise, all the ground terms that can be created with the give funcs and that contain only n function symbols.

Returns all ground terms that can be created from constant terms cntms and functions symbols funcs involving n function symbols.

If n = 0, it returns the constant terms, otherwise tries all possible functions.

cntms : term list

The input list of constant terms.

funcs : (string * int) list

The input list of function name-arity pairs.

n : int

The number of function symbols the resulting ground terms will contain.

Returns: term list

The input cntms itself, if n is 0; otherwise, all the ground terms that can be created with the give funcs and that contain only n function symbols.

Example 

 groundterms !!!>["0";"1"] [("f",1);("g",2)] 0
Evaluates to 
 [``0``; ``1``]

Example 

 groundterms !!!>["0";"1"] [("f",1);("g",2)] 1
Evaluates to 
 [``f(0)``; ``f(1)``; ``g(0,0)``; 
  ``g(0,1)``; ``g(1,0)``; ``g(1,1)``]

Example 

 groundterms !!!>["0";"1"] [("f",1);("g",2)] 2
Evaluates to 
 [``f(f(0))``; ``f(f(1))``; ``f(g(0,0))``; 
  ``f(g(0,1))``; ``f(g(1,0))``; ``f(g(1,1))``; 
  ``g(0,f(0))``; ``g(0,f(1))``; ``g(0,g(0,0))``;
  ``g(0,g(0,1))``; ``g(0,g(1,0))``; ``g(0,g(1,1))``; 
  ``g(1,f(0))``; ``g(1,f(1))``; ``g(1,g(0,0))``; 
  ``g(1,g(0,1))``; ``g(1,g(1,0))``;``g(1,g(1,1))``; 
  ``g(f(0),0)``; ``g(f(0),1)``; ``g(f(1),0)``; 
  ``g(f(1),1)``; ``g(g(0,0),0)``; ``g(g(0,0),1)``; 
  ``g(g(0,1),0)``; ``g(g(0,1),1)``;``g(g(1,0),0)``; 
  ``g(g(1,0),1)``; ``g(g(1,1),0)``; ``g(g(1,1),1)``]

groundtuples cntms funcs n m

Full Usage: groundtuples cntms funcs n m

Parameters:
    cntms : term list - The input list of constant terms.
    funcs : (string * int) list - The input list of function name-arity pairs.
    n : int - The number of function symbols the resulting ground terms will contain.
    m : int - The number of element of the resulting ground terms tuples.

Returns: term list list All the m-tuples of ground terms that can be created from then input cntms and funcs where each ground term contain only n function symbols.

Returns all the m-tuples of ground terms that can be created from constant terms cntms and functions symbols funcs involving n function symbols.

cntms : term list

The input list of constant terms.

funcs : (string * int) list

The input list of function name-arity pairs.

n : int

The number of function symbols the resulting ground terms will contain.

m : int

The number of element of the resulting ground terms tuples.

Returns: term list list

All the m-tuples of ground terms that can be created from then input cntms and funcs where each ground term contain only n function symbols.

Example 

 groundtuples !!!>["0";"1"] [("f",1);("g",2)] 0 2
Evaluates to 
 [[``0``; ``0``]; [``0``; ``1``]; 
  [``1``; ``0``]; [``1``; ``1``]]

Example 

 groundtuples !!!>["0";"1"] [("f",1);("g",2)] 2 3
Evaluates to 
 [[``0``; ``0``; ``f(f(0))``]; 
 [``0``; ``0``; ``f(f(1))``];
 [``0``; ``0``; ``f(g(0,0))``]; 
 [``0``; ``0``; ``f(g(0,1))``];
 [``0``; ``0``; ``f(g(1,0))``]; 
 ...
 [``1``; ``g(g(0,1),0)``; ``0``];
 ...
 [``g(g(1,1),1)``; ``1``; ``1``]]

herbfuns fm

Full Usage: herbfuns fm

Parameters:
Returns: (string * int) list * (string * int) list The pair of lists of functions in the formula separated in nullary and non.

Returns the functions in the formula fm separated in nullary and non, and adding nullary one if necessary.

fm : formula<fol>

The input formula.

Returns: (string * int) list * (string * int) list

The pair of lists of functions in the formula separated in nullary and non.

Example 

 !!"forall x. P(x) /\ (Q(f(y)) ==> R(g(x,y),z))"
 |> herbfuns
Evaluates to ([("c", 0)], [("f", 1); ("g", 2)]).

Herbrand procedures

Functions and values

Function or value Description

herbloop mfn tfn fl0 cntms funcs fvs n fl tried tuples

Full Usage: herbloop mfn tfn fl0 cntms funcs fvs n fl tried tuples

Parameters:
    mfn : 'a -> (formula<fol> -> formula<fol>) -> formula<fol> list list -> formula<fol> list list - The modification function that augments the ground instances with a new instance.
    tfn : formula<fol> list list -> bool - The satisfiability test to be done.
    fl0 : 'a - The input set of clauses: i.e. a formula in some transformed list representation.
    cntms : term list - The constant terms to generate the ground terms.
    funcs : (string * int) list - The function symbols (name, arity) to generate the ground terms.
    fvs : string list - The free variables to instantiate to generate the ground terms.
    n : int - The number of function symbols the new ground terms to be generated should contain.
    fl : formula<fol> list list - The set of ground instances so far.
    tried : term list list - The instances tried.
    tuples : term list list - The remaining ground instances in the current level.

Returns: term list list The list of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Tests the unsatisfiability of a set of clauses.

This is a generic function to be used with different 'herbrand procedures'.

It tests larger and larger conjunctions of ground instances for unsatisfiability, iterating the given modifier function mfn over ground terms till the given test function tfn fails.

mfn : 'a -> (formula<fol> -> formula<fol>) -> formula<fol> list list -> formula<fol> list list

The modification function that augments the ground instances with a new instance.

tfn : formula<fol> list list -> bool

The satisfiability test to be done.

fl0 : 'a

The input set of clauses: i.e. a formula in some transformed list representation.

cntms : term list

The constant terms to generate the ground terms.

funcs : (string * int) list

The function symbols (name, arity) to generate the ground terms.

fvs : string list

The free variables to instantiate to generate the ground terms.

n : int

The number of function symbols the new ground terms to be generated should contain.

fl : formula<fol> list list

The set of ground instances so far.

tried : term list list

The instances tried.

tuples : term list list

The remaining ground instances in the current level.

Returns: term list list

The list of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Note

See the specific implementations Herbrand.gilmore_loop, Herbrand.dp_loop, Herbrand.dp_refine_loop for examples.

A gilmore-like procedure

Functions and values

Function or value Description

gilmore fm

Full Usage: gilmore fm

Parameters:
Returns: int The number of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops indefinitely till the memory is full.

Tests the validity of a formula with a Gilmore-like procedure.

fm : formula<fol>

The input formula.

Returns: int

The number of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops indefinitely till the memory is full.

Note

The procedure loops infinitely if the initial formula is not valid and even if it is, it is not guaranteed to end.

Example 

 gilmore !! "exists x. forall y. P(x) ==> P(y)"
Evaluates to 2 and print to the stdout: 
 0 ground instances tried; 1 items in list.
 0 ground instances tried; 1 items in list.
 1 ground instances tried; 1 items in list.
 1 ground instances tried; 1 items in list.
type 'T list = List<'T>

gilmore_loop fl0 cntms funcs fvs n fl tried tuples

Full Usage: gilmore_loop fl0 cntms funcs fvs n fl tried tuples

Parameters:
    fl0 : formula<fol> list list - The input set of clauses.
    cntms : term list - The constant terms to generate the ground terms.
    funcs : (string * int) list - The function symbols (name, arity) to generate the ground terms.
    fvs : string list - The free variables to instantiate to generate the ground terms.
    n : int - The number of function symbols the new ground terms to be generated should contain.
    fl : formula<fol> list list - The set of ground instances so far.
    tried : term list list - The instances tried.
    tuples : term list list - The remaining ground instances in the current level.

Returns: term list list The list of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Tests the unsatisfiability of a set of clauses with a Gilmore-like procedure.

The input set of clauses fl0 is intended to represent a DNF formula and cntms, funcs and fvs are supposed to be the constant and function symbols and the free variables of the formula, respectively. The function implements an Herbrand.herbloop specific for the Gilmore procedure, calling it with the specific gilmore modification and test functions.

fl0 : formula<fol> list list

The input set of clauses.

cntms : term list

The constant terms to generate the ground terms.

funcs : (string * int) list

The function symbols (name, arity) to generate the ground terms.

fvs : string list

The free variables to instantiate to generate the ground terms.

n : int

The number of function symbols the new ground terms to be generated should contain.

fl : formula<fol> list list

The set of ground instances so far.

tried : term list list

The instances tried.

tuples : term list list

The remaining ground instances in the current level.

Returns: term list list

The list of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Example 

 gilmore_loop !!>>[["Q(f_z(x))"; "~Q(y)"]] 
   !!!>["c"] [("f_z",1);("f_y",1)] ["x";"y"] 0 [[]] [] []
Evaluates to [[``c``; ``f_z(c)``]; [``c``; ``c``]] and print to the stdout: 
 0 ground instances tried; 1 items in list.
 0 ground instances tried; 1 items in list.
 1 ground instances tried; 1 items in list.
 1 ground instances tried; 1 items in list.
type 'T list = List<'T>

gilmore_mfn djs0 ifn djs

Full Usage: gilmore_mfn djs0 ifn djs

Parameters:
    djs0 : formula<fol> list list - The input formula in DNF 'clausal' form.
    ifn : formula<fol> -> formula<fol> - The instantiation function.
    djs : formula<fol> list list - The ground instance of the input formula so far.

Returns: formula<fol> list list The updated ground instance of the input formula.

Generates the ground instances for the Gilmore procedure.

Updates the ground instance djs of the initial formula in DNF 'clausal' form djs0 with the new ground terms generated from the given instantiation ifn.

Since we are in a DNF context, a list of clauses here is an iterated disjunction of conjunctions and so each clause is a conjunction. The ground instances generated for each of the conjunctions are added as new conjuncts to the corresponding conjunction, deleting those that become contradictory due to the presence of complementary literals.

djs0 : formula<fol> list list

The input formula in DNF 'clausal' form.

ifn : formula<fol> -> formula<fol>

The instantiation function.

djs : formula<fol> list list

The ground instance of the input formula so far.

Returns: formula<fol> list list

The updated ground instance of the input formula.

Example

In this example each conjunct in the original formula P(f(x)) \/ ~P(y) is just a literal. As new ground terms are generated, each conjunction becomes the conjunction of all ground instances generated so far for the corresponding original literal. 

 gilmore_mfn !!>>[["P(f(x))"]; ["~P(y)"]] 
   (subst (fpf ["x"; "y"] !!!>["c";"f(c)"])) 
   !!>>[["P(f(c))"]; ["~P(c)"]]
Evaluates to 
 [[`P(f(c))`]; [`P(f(c))`; `~P(c)`]; [`~P(c)`; `~P(f(c))`]]
Corresponding to the formula `P(f(c)) \/ P(f(c)) /\ ~P(c) \/ ~P(c) /\ ~P(f(c))`.

Note that the input ground instance [["P(f(c))"]; ["~P(c)"]] must have been generated by an instantiation that mapped both x and y to c while the new given instantiation maps y to f(c).

Note also that the conjunct [`P(f(c))`; `~P(f(c))`] has been removed from the output, since contradictory.

gilmore_tfn djs

Full Usage: gilmore_tfn djs

Parameters:
    djs : 'a list - The input formula (more precisely its ground instance so far) in a DNF 'clausal' form.

Returns: bool true, if the input is nonempty; otherwise, false

Gilmore test function: tests if the input set of clauses is nonempty.

It simply tests that the set of DNF 'clauses' is nonempty, because the contradiction checking is done by the modification function.

djs : 'a list

The input formula (more precisely its ground instance so far) in a DNF 'clausal' form.

Returns: bool

true, if the input is nonempty; otherwise, false

Example 

 !!>>[["P(f(c))"]; ["P(f(c))"; "~P(c)"]; ["P(f(c))"; "~P(f(c))"];
    ["~P(c)"; "~P(f(c))"]]
 |> gilmore_tfn
Evaluates to true.

Example 

 !!>>[]
Evaluates to false.

The Davis-Putnam procedure for first order logic

Functions and values

Function or value Description

davisputnam fm

Full Usage: davisputnam fm

Parameters:
Returns: int The number of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops indefinitely till the memory is full.

Tests the validity of a formula with the Davis-Putnam procedure.

fm : formula<fol>

The input formula.

Returns: int

The number of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops indefinitely till the memory is full.

Note

The procedure loops infinitely if the initial formula is not valid and even if it is, it is not guaranteed to end.

Example 

 davisputnam !! "exists x. forall y. P(x) ==> P(y)"
Evaluates to 2 and print to the stdout: 
 0 ground instances tried; 0 items in list.
 0 ground instances tried; 0 items in list.
 1 ground instances tried; 2 items in list.
 1 ground instances tried; 2 items in list.
type 'T list = List<'T>

dp_loop fl0 cntms funcs fvs n fl tried tuples

Full Usage: dp_loop fl0 cntms funcs fvs n fl tried tuples

Parameters:
    fl0 : formula<fol> list list - The input set of clauses.
    cntms : term list - The constant terms to generate the ground terms.
    funcs : (string * int) list - The function symbols (name, arity) to generate the ground terms.
    fvs : string list - The free variables to instantiate to generate the ground terms.
    n : int - The number of function symbols the new ground terms to be generated should contain.
    fl : formula<fol> list list - The set of ground instances so far.
    tried : term list list - The instances tried.
    tuples : term list list - The remaining ground instances in the current level.

Returns: term list list The list of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Tests the unsatisfiability of a set of clauses with the Davis-Putnam procedure.

The input set of clauses fl0 is intended to represent a CNF formula and cntms, funcs and fvs are supposed to be the constant and function symbols and the free variables of the formula, respectively. The function implements an Herbrand.herbloop specific for the Davis-Putnam procedure, calling it with the specific Davis-Putnam modification function Herbrand.dp_mfn and using DP.dpll as test function.

fl0 : formula<fol> list list

The input set of clauses.

cntms : term list

The constant terms to generate the ground terms.

funcs : (string * int) list

The function symbols (name, arity) to generate the ground terms.

fvs : string list

The free variables to instantiate to generate the ground terms.

n : int

The number of function symbols the new ground terms to be generated should contain.

fl : formula<fol> list list

The set of ground instances so far.

tried : term list list

The instances tried.

tuples : term list list

The remaining ground instances in the current level.

Returns: term list list

The list of ground tuples generated and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Example 

 dp_loop !!>>[["P(x)"]; ["~P(f_y(y))"]]
     !!!>["c"] [("f_y",1);] ["x";"y"] 0 [] [] []
Evaluates to [[``f_y(c)``; ``c``]; [``c``; ``f_y(c)``]; [``c``; ``c``]] and print to the stdout: 
 0 ground instances tried; 0 items in list.
 0 ground instances tried; 0 items in list.
 1 ground instances tried; 2 items in list.
 1 ground instances tried; 2 items in list.
 2 ground instances tried; 3 items in list.
type 'T list = List<'T>

dp_mfn cjs0 ifn cjs

Full Usage: dp_mfn cjs0 ifn cjs

Parameters:
    cjs0 : 'a list list - The initial formula in a list of list representation of conjunctive normal.
    ifn : 'a -> 'b - The instantiation to be applied to the formula to generate ground instances.
    cjs : 'b list list - The set of ground instances so far.

Returns: 'b list list The set of ground instances incremented.

Generates the ground instances for the Davis-Putnam procedure.

cjs0 : 'a list list

The initial formula in a list of list representation of conjunctive normal.

ifn : 'a -> 'b

The instantiation to be applied to the formula to generate ground instances.

cjs : 'b list list

The set of ground instances so far.

Returns: 'b list list

The set of ground instances incremented.

Example

This example shows the first generation of ground instance when the set is initially empty. 

 dp_mfn !!>>[["P(x)"]; ["~P(f_y(x))"]] 
   (subst (fpf ["x"] [!!!"c"])) []
Evaluates to [[`P(c)`]; [`~P(f_y(c))`]].

Example

This example shows the second generation of ground instance when the nonempty set is augmented. 

 dp_mfn !!>>[["P(x)"]; ["~P(f_y(x))"]] 
   (subst (fpf ["x"] [!!!"f_y(c)"])) 
   !!>>[["P(c)"]; ["~P(f_y(c))"]]
Evaluates to [[`P(c)`]; [`P(f_y(c))`]; [`~P(f_y(c))`]; [`~P(f_y(f_y(c)))`]].

The Davis-Putnam procedure refined

Functions and values

Function or value Description

davisputnam002 fm

Full Usage: davisputnam002 fm

Parameters:
Returns: int The number of ground tuples needed to prove the validity and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops indefinitely till the memory is full.

Tests the validity of a formula with the Davis-Putnam procedure refined.

The difference with Herbrand.davisputnam is just that the number returned is not the number of ground instance generated but that of those that are really needed.

fm : formula<fol>

The input formula.

Returns: int

The number of ground tuples needed to prove the validity and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops indefinitely till the memory is full.

Note

The procedure loops infinitely if the initial formula is not valid and even if it is, it is not guaranteed to end.

Example 

 davisputnam002 p36
Evaluates to 3 and print to the stdout: 
 0 ground instances tried; 0 items in list.
 0 ground instances tried; 0 items in list.
 1 ground instances tried; 6 items in list.
 ...
 37 ground instances tried; 168 items in list.
 38 ground instances tried; 172 items in list.
 39 ground instances tried; 176 items in list.
type 'T list = List<'T>

dp_refine cjs0 fvs dunno need

Full Usage: dp_refine cjs0 fvs dunno need

Parameters:
    cjs0 : formula<fol> list list - The input set of clauses.
    fvs : string list - The free variables to instantiate to generate the ground terms.
    dunno : term list list - The list of possibly-needed instances.
    need : term list list - The list of really needed instances.

Returns: term list list The list of really needed instances to refute the input set of clauses, if there is one; otherwise, the input dunno itself in reverse order.

Returns the list of ground tuples that are really needed to refute cjs0.

cjs0 : formula<fol> list list

The input set of clauses.

fvs : string list

The free variables to instantiate to generate the ground terms.

dunno : term list list

The list of possibly-needed instances.

need : term list list

The list of really needed instances.

Returns: term list list

The list of really needed instances to refute the input set of clauses, if there is one; otherwise, the input dunno itself in reverse order.

Example 

 dp_refine !!>>[["P(x)"]; ["~P(f_y(y))"]] ["x";"y"] 
   !!!>>[["f_y(c)"; "c"]; ["c";"c"]; ["d";"d"]] []
Evaluates to [[``f_y(c)``]; [``c``]].

dp_refine_loop cjs0 cntms funcs fvs n cjs tried tuples

Full Usage: dp_refine_loop cjs0 cntms funcs fvs n cjs tried tuples

Parameters:
    cjs0 : formula<fol> list list
    cntms : term list - The constant terms to generate the ground terms.
    funcs : (string * int) list - The function symbols (name, arity) to generate the ground terms.
    fvs : string list - The free variables to instantiate to generate the ground terms.
    n : int - The number of function symbols the new ground terms to be generated should contain.
    cjs : formula<fol> list list
    tried : term list list - The instances tried.
    tuples : term list list - The remaining ground instances in the current level.

Returns: term list list The list of ground tuples needed to refute the input and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Tests the unsatisfiability of a set of clauses with the Davis-Putnam procedure refined.

The difference with Herbrand.dp_loop is just that the list returned is not the number of ground tuples generated but of those that are really needed to refute the input.

cjs0 : formula<fol> list list
cntms : term list

The constant terms to generate the ground terms.

funcs : (string * int) list

The function symbols (name, arity) to generate the ground terms.

fvs : string list

The free variables to instantiate to generate the ground terms.

n : int

The number of function symbols the new ground terms to be generated should contain.

cjs : formula<fol> list list
tried : term list list

The instances tried.

tuples : term list list

The remaining ground instances in the current level.

Returns: term list list

The list of ground tuples needed to refute the input and prints to the stdout how many ground instances were tried, if the procedure terminates (thus indicating that the formula is valid); otherwise, loops generating and testing larger and larger ground instances till the memory is full.

Example 

 dp_refine_loop !!>>[["P(x)"]; ["~P(f_y(y))"]]
     !!!>["c"] [("f_y",1);] ["x";"y"] 0 [] [] []
Evaluates to [[``f_y(c)``; ``c``]] and print to the stdout: 
 0 ground instances tried; 0 items in list.
 0 ground instances tried; 0 items in list.
 1 ground instances tried; 2 items in list.
 1 ground instances tried; 2 items in list.
 2 ground instances tried; 3 items in list.
type 'T list = List<'T>