Calculemus

Meson Module

Namespace: Calculemus
Assembly: Calculemus.dll

Model elimination procedure (MESON version, based on Stickel's PTTP).

Table of contents

Basic MESON procedure

Functions and values

Function or value Description

contrapositives cls

Full Usage: contrapositives cls

Parameters:
    cls : formula<'a> list - The input clause.

Returns: (formula<'a> list * formula<'a>) list The set of contrapositives of the input clause.

Converts a clause into the set of all its contrapositives.

If the clause is completely negative, is also added the rule with false as conclusion.

cls : formula<'a> list

The input clause.

Returns: (formula<'a> list * formula<'a>) list

The set of contrapositives of the input clause.

Example 

 contrapositives !!>["P";"Q";"~R"]
Evaluates to [([`~Q`; `R`], `P`); ([`~P`; `R`], `Q`); ([`~P`; `~Q`], `~R`)].

Example 

 contrapositives !!>["~P";"~Q";"~R"]
Evaluates to [([`P`; `Q`; `R`], `false`); ([`Q`; `R`], `~P`); ([`P`; `R`], `~Q`); ([`P`; `Q`], `~R`)].

meson_basic fm

Full Usage: meson_basic fm

Parameters:
Returns: int list the list of depth limits reached trying to refute the subproblems, if the formula is valid.

Tests the validity of a formula by negating it and splitting in subproblems to be refuted with the core MESON procedure.

fm : formula<fol>

The input formula.

Returns: int list

the list of depth limits reached trying to refute the subproblems, if the formula is valid.

Note

Prints the depth limits tried to the stdout. Crashes if the input formula is not unsatisfiable.

Example 

 !! @"exists x. exists y. forall z.
     (F(x,y) ==> (F(y,z) /\ F(z,z))) /\
     ((F(x,y) /\ G(x,y)) ==> (G(x,z) /\ G(z,z)))"
 |> meson_basic
Evaluates to [8] and prints to the stdout: 
 Searching with depth limit 1
 Searching with depth limit 2
 Searching with depth limit 3
 Searching with depth limit 4
 Searching with depth limit 5
 Searching with depth limit 6
 Searching with depth limit 7
 Searching with depth limit 8

mexpand_basic rules ancestors g cont (env, n, k)

Full Usage: mexpand_basic rules ancestors g cont (env, n, k)

Parameters:
    rules : (formula<fol> list * formula<fol>) list - The input list of rules.
    ancestors : formula<fol> list - The accumulator for the ancestors.
    g : formula<fol> - The goal to be solved from the rules.
    cont : func<string, term> * int * int -> func<string, term> * int * int - The continuation function to solve the subgoals.
    env : func<string, term> - The given instantiation under which trying solving.
    n : int - The maximum number of rule applications permitted.
    k : int - The counter for variable renaming.

Returns: func<string, term> * int * int The triple with the current instantiation, the depth reached and the number of variables renamed.

Core MESON engine.

It tries to solve the input goal g according to the rules with the following steps:

  • If the current size bound has been exceeded, fail;
  • otherwise, try to unify the current goal with the negation of one of its ancestors (not renaming variables) and call cont to do the same for the remaining goals under the new instantiation;
  • if this fails, try a normal Prolog-style extension with one of the rules, first unifying with a renamed rule and then iterating recursive calls over the list of subgoals, with the environment modified according to the results of unification, the permissible number of new nodes decreased by the number of new subgoals created, and the variable renaming counter increased.

rules : (formula<fol> list * formula<fol>) list

The input list of rules.

ancestors : formula<fol> list

The accumulator for the ancestors.

g : formula<fol>

The goal to be solved from the rules.

cont : func<string, term> * int * int -> func<string, term> * int * int

The continuation function to solve the subgoals.

env : func<string, term>

The given instantiation under which trying solving.

n : int

The maximum number of rule applications permitted.

k : int

The counter for variable renaming.

Returns: func<string, term> * int * int

The triple with the current instantiation, the depth reached and the number of variables renamed.

Exception Thrown with message Too deep when n < 0.
Exception Thrown with message tryfind when the goals are not solvable, at least at the current limit.
Note

See also Prolog.backchain, Tableaux.tableau

Example 

 mexpand_basic 
   [
       ([], !!"P(x)"); 
       ([!!"P(x)"], False);
   ]
   [] False id (undefined,1,0)
 |> fun (env,n,k) -> (graph env,n,k)
val id: x: 'T -> 'T
val env: obj
val n: obj
val k: obj
Evaluates to ([("_0", ``_1``)], 0, 2).

Example 

 mexpand_basic 
   [
       ([], !!"P(x)"); 
       ([!!"P(x)"], False);
   ]
   [] False id (undefined,0,0)
val id: x: 'T -> 'T
Throws System.Exception: tryfind.

Example 

 mexpand_basic 
   [
       ([], !!"P(x)"); 
       ([!!"P(x)"], False);
   ]
   [] False id (undefined,-1,0)
val id: x: 'T -> 'T
Throws System.Exception: Too deep.

puremeson_basic fm

Full Usage: puremeson_basic fm

Parameters:
Returns: int the number of depth limit reached trying refuting the formula with MESON, if the input formula is unsatisfiable and a refutation could be found.

Tests the unsatisfiability of a formula using the core MESON procedure.

fm : formula<fol>

The input formula.

Returns: int

the number of depth limit reached trying refuting the formula with MESON, if the input formula is unsatisfiable and a refutation could be found.

Note

Prints the depth limits tried to the stdout. Crashes if the input formula is not unsatisfiable.

Example 

 !!"P(x) /\ ~P(x)"
 |> puremeson_basic
Evaluates to 1 and prints to the stdout: 
 Searching with depth limit 0
 Searching with depth limit 1

MESON procedure optimized

Functions and values

Function or value Description

equal env fm1 fm2

Full Usage: equal env fm1 fm2

Parameters:
    env : func<string, term> - The given instantiation.
    fm1 : formula<fol> - The first input literal.
    fm2 : formula<fol> - The second input literal.

Returns: bool true, if the input formulas are literals and identical under the give instantiation; otherwise, false (this is the case also if the input formulas are identical but not literals).

Tests if two literals are identical under the given instantiation.

env : func<string, term>

The given instantiation.

fm1 : formula<fol>

The first input literal.

fm2 : formula<fol>

The second input literal.

Returns: bool

true, if the input formulas are literals and identical under the give instantiation; otherwise, false (this is the case also if the input formulas are identical but not literals).

Example

Identical literals 

 equal 
   (("x" |-> !!!"f(y)")undefined) 
   !!"P(x)" !!"P(f(y))"
Evaluates to true.

Example

Different literals 

 equal 
   (("x" |-> !!!"f(z)")undefined) 
   !!"P(x)" !!"P(f(y))"
Evaluates to false.

Example

Identical formulas that are not literals 

 equal 
   (("x" |-> !!!"f(y)")undefined) 
   !!"P(x) /\ P(x)" !!"P(f(y)) /\ P(f(y))"
Evaluates to false.

expand2 expfn goals1 n1 goals2 n2 n3 cont env k

Full Usage: expand2 expfn goals1 n1 goals2 n2 n3 cont env k

Parameters:
    expfn : formula<fol> list -> (func<string, term> * int * int -> func<string, term> * int * int) -> func<string, term> * int * int -> func<string, term> * int * int - The input basic expansion.
    goals1 : formula<fol> list - The first list of subgoals.
    n1 : int - The depth limit for goals1.
    goals2 : formula<fol> list - The second list of subgoals.
    n2 : int - The depth limit for goals2 that will be added to what is left from goals1.
    n3 : int - The minimum depth limit allowed for goals2.
    cont : func<string, term> * int * int -> func<string, term> * int * int - The supporting continuation function.
    env : func<string, term> - The given instantiation under which trying solving.
    k : int - The counter for variable renaming.

Returns: func<string, term> * int * int The triple with the current instantiation, the depth reached and the number of variables renamed.

Optimizes the depth limit used by a basic expansion.

Applies expfn to goals1 with size limit n1, then attempts goals2 with whatever is left over from goals1 plus an additional n2, yet forces the continuation to fail unless the second takes more than n3.

expfn : formula<fol> list -> (func<string, term> * int * int -> func<string, term> * int * int) -> func<string, term> * int * int -> func<string, term> * int * int

The input basic expansion.

goals1 : formula<fol> list

The first list of subgoals.

n1 : int

The depth limit for goals1.

goals2 : formula<fol> list

The second list of subgoals.

n2 : int

The depth limit for goals2 that will be added to what is left from goals1.

n3 : int

The minimum depth limit allowed for goals2.

cont : func<string, term> * int * int -> func<string, term> * int * int

The supporting continuation function.

env : func<string, term>

The given instantiation under which trying solving.

k : int

The counter for variable renaming.

Returns: func<string, term> * int * int

The triple with the current instantiation, the depth reached and the number of variables renamed.

Exception Thrown with message pair when... TODO

meson fm

Full Usage: meson fm

Parameters:
Returns: int list the list of depth limits reached trying to refute the subproblems, if the formula is valid.

Tests the validity of a formula by negating it and splitting in subproblems to be refuted with the core MESON procedure optimized.

fm : formula<fol>

The input formula.

Returns: int list

the list of depth limits reached trying to refute the subproblems, if the formula is valid.

Note

Prints the depth limits tried to the stdout. Crashes if the input formula is not unsatisfiable.

Example 

 !! @"exists x. exists y. forall z.
     (F(x,y) ==> (F(y,z) /\ F(z,z))) /\
     ((F(x,y) /\ G(x,y)) ==> (G(x,z) /\ G(z,z)))"
 |> meson
Evaluates to [8] and prints to the stdout: 
 Searching with depth limit 1
 Searching with depth limit 2
 Searching with depth limit 3
 Searching with depth limit 4
 Searching with depth limit 5
 Searching with depth limit 6
 Searching with depth limit 7
 Searching with depth limit 8

mexpand rules ancestors g cont (env, n, k)

Full Usage: mexpand rules ancestors g cont (env, n, k)

Parameters:
    rules : (formula<fol> list * formula<fol>) list - The input list of rules.
    ancestors : formula<fol> list - The accumulator for the ancestors.
    g : formula<fol> - The goal to be solved from the rules.
    cont : func<string, term> * int * int -> func<string, term> * int * int - The continuation function to solve the subgoals.
    env : func<string, term> - The given instantiation under which trying solving.
    n : int - The maximum number of rule applications permitted.
    k : int - The counter for variable renaming.

Returns: func<string, term> * int * int The triple with the current instantiation, the depth reached and the number of variables renamed.

Core MESON engine optimized with Meson.expand2.

... TODO

rules : (formula<fol> list * formula<fol>) list

The input list of rules.

ancestors : formula<fol> list

The accumulator for the ancestors.

g : formula<fol>

The goal to be solved from the rules.

cont : func<string, term> * int * int -> func<string, term> * int * int

The continuation function to solve the subgoals.

env : func<string, term>

The given instantiation under which trying solving.

n : int

The maximum number of rule applications permitted.

k : int

The counter for variable renaming.

Returns: func<string, term> * int * int

The triple with the current instantiation, the depth reached and the number of variables renamed.

Exception Thrown with message Too deep when n < 0.
Exception Thrown with message tryfind when the goals are not solvable, at least at the current limit.
Exception Thrown with message repetition when... TODO
Example 

 mexpand 
   [
       ([], !!"P(x)"); 
       ([!!"P(x)"], False);
   ]
   [] False id (undefined,1,0)
 |> fun (env,n,k) -> (graph env,n,k)
val id: x: 'T -> 'T
val env: obj
val n: obj
val k: obj
Evaluates to ([("_0", ``_1``)], 0, 2).

Example 

 mexpand 
   [
       ([], !!"P(x)"); 
       ([!!"P(x)"], False);
   ]
   [] False id (undefined,0,0)
val id: x: 'T -> 'T
Throws System.Exception: tryfind.

Example 

 mexpand 
   [
       ([], !!"P(x)"); 
       ([!!"P(x)"], False);
   ]
   [] False id (undefined,-1,0)
val id: x: 'T -> 'T
Throws System.Exception: Too deep.

puremeson fm

Full Usage: puremeson fm

Parameters:
Returns: int the number of depth limit reached trying refuting the formula with MESON, if the input formula is unsatisfiable and a refutation could be found.

Tests the unsatisfiability of a formula using the core MESON procedure optimized.

fm : formula<fol>

The input formula.

Returns: int

the number of depth limit reached trying refuting the formula with MESON, if the input formula is unsatisfiable and a refutation could be found.

Note

Prints the depth limits tried to the stdout. Crashes if the input formula is not unsatisfiable.

Example 

 !!"P(x) /\ ~P(x)"
 |> puremeson
Evaluates to 1 and prints to the stdout: 
 Searching with depth limit 0
 Searching with depth limit 1