Tableaux (Calculemus)

Tableaux Module

Namespace: Calculemus
Assembly: Calculemus.dll

Tableaux, seen as an optimized version of a Prawitz-like procedure.

Unification of literals
Refutation via unification
Prawitz procedure
Tableaux procedure
Tableaux procedure optimized

Unification of literals

Functions and values

Function or value Description


                
                  
                    
                      unify_complements env (p, q)

Full Usage: unify_complements env (p, q)

Parameters:

env : func<string, term> - An environment of mappings (represented as a finite partial function) from variables to terms, used as an accumulator for the final result of the unification procedure.

p : formula<fol> - The first input literal.

q : formula<fol> - The second input literal.

Returns: func<string, term> The instantiation that makes the input literals become complementary, if such an instantiation exists.

Returns a unifier for a complementary pair of literals.

env : func<string, term>: An environment of mappings (represented as a finite partial function) from variables to terms, used as an accumulator for the final result of the unification procedure.
p : formula<fol>: The first input literal.
q : formula<fol>: The second input literal.

Returns: func<string, term>: The instantiation that makes the input literals become complementary, if such an instantiation exists.

Exception	Thrown with message `cyclic` when there is a cyclic assignment.
Exception	Thrown with message `impossible unification` when the unification is not possible.
Exception	Thrown with message `Can't unify literals` when the input `eq` is neither a pair of literal or the degenerated case `False,False`

Example

Successful unification

 unify_complements undefined (!!"P(x)",!!"~P(f(y))")
 |> graph

Evaluates to [("x", ``f(y)``)].

Example

Cyclic assignment

 unify_complements undefined (!!"P(y)",!!"~P(f(y))")

Throws System.Exception: cyclic.

Example

Impossible unification

 unify_complements undefined (!!"P(g(x))",!!"~P(f(y))")

Throws System.Exception: impossible unification.

Example

Invalid input

 unify_literals undefined (!!"P(x) /\ Q(x)",!!"~P(f(y))")

Throws System.Exception: Can't unify literals.


                
                  
                    
                      unify_literals env (p, q)

Full Usage: unify_literals env (p, q)

Parameters:

p : formula<fol> - The first input literal.

q : formula<fol> - The second input literal.

Returns: func<string, term> A variable-term mappings that unify eq, if the unification is possible and there are no cycles.

Returns a unifier for a pair of literals.

It also handles the pair False,False.

env : func<string, term>: An environment of mappings (represented as a finite partial function) from variables to terms, used as an accumulator for the final result of the unification procedure.
p : formula<fol>: The first input literal.
q : formula<fol>: The second input literal.

Returns: func<string, term>: A variable-term mappings that unify eq, if the unification is possible and there are no cycles.

Exception	Thrown with message `cyclic` when there is a cyclic assignment.
Exception	Thrown with message `impossible unification` when the unification is not possible.
Exception	Thrown with message `Can't unify literals` when the input `eq` is neither a pair of literal or the degenerated case `False,False`

Example

Successful unification

 unify_literals undefined (!!"P(x)",!!"P(f(y))")
 |> graph

Evaluates to [("x", ``f(y)``)].

Example

Degenerated case

 unify_literals undefined (!!"false",!!"false")
 |> graph

Evaluates to [].

Example

Cyclic assignment

 unify_literals undefined (!!"P(y)",!!"P(f(y))")

Throws System.Exception: cyclic.

Example

Impossible unification

 unify_literals undefined (!!"P(g(x))",!!"P(f(y))")

Throws System.Exception: impossible unification.

Example

Invalid input

 unify_literals undefined (!!"P(x)",!!"~P(f(y))")

Throws System.Exception: Can't unify literals.

Refutation via unification

Functions and values

Function or value Description


                
                  
                    
                      unify_refute djs env

Full Usage: unify_refute djs env

Parameters:

djs : formula<fol> list list - The input DNF list of clauses

Returns: func<string, term> The variable-term mappings that causes each clause to contain complementary literals, if this mapping exists.

Returns a unifier that causes each clause in the input list to contain complementary literals.

djs : formula<fol> list list: The input DNF list of clauses
env : func<string, term>: An environment of mappings (represented as a finite partial function) from variables to terms, used as an accumulator for the final result of the unification procedure.

Returns: func<string, term>: The variable-term mappings that causes each clause to contain complementary literals, if this mapping exists.

Exception Thrown with message tryfind when there isn't any such mapping.

Example

Successful refutation

 undefined
 |> unify_refute !!>>[
         ["P(x)";"~P(f(y))";"R(x,y)"];
         ["Q(x)";"~Q(x)"]
 ]
 |> graph

Evaluates to [("x", ``f(y)``)].

Example

Failing refutation

 undefined
 |> unify_refute !!>>[["P(c)"];["Q(c)"]]

Throws to System.Exception: tryfind.

Prawitz procedure

Functions and values

Function or value	Description
`prawitz fm` Full Usage: `prawitz fm` Parameters: fm : `formula<fol>` - The input formula. Returns: `int` The number of instance tried.	Tests the validity of a formula with a Prawitz-like procedure. fm : `formula<fol>` The input formula. Returns: `int` The number of instance tried. Example `prawitz Pelletier.p20` Evaluates to `2`.
`prawitz_loop djs0 fvs djs n` Full Usage: `prawitz_loop djs0 fvs djs n` Parameters: djs0 : `formula<fol> list list` - The input set of clauses. fvs : `string list` - The free variables to unify. djs : `formula<fol> list list` - The accumulator for the substitution instances. n : `int` - A counter to generate fresh variable names. Returns: `func<string, term> * int` The final instantiation together with the number of instances tried.	Tests the unsatisfiability of a set of clauses with a Prawitz-like procedure. The input set of clauses `djs0` is intended to represent a DNF formula and `fvs` are supposed to be the free variables of the formula. djs0 : `formula<fol> list list` The input set of clauses. fvs : `string list` The free variables to unify. djs : `formula<fol> list list` The accumulator for the substitution instances. n : `int` A counter to generate fresh variable names. Returns: `func<string, term> * int` The final instantiation together with the number of instances tried. Example Successful refutation `prawitz_loop !!>>[ ["P(x)";"~P(f(y))";"R(x,y)"]; ["Q(x)";"~Q(x)"] ] ["x";"y"] [[]] 0 \|> fun (env,nr) -> env \|> graph, nr` val env: obj val nr: obj Evaluates to [("x", ``f(y)``)].

Tableaux procedure

Functions and values

Function or value Description

Full Usage: deepen f n

Parameters:

f : int -> 'a - The input function.

n : int - The input integer.

Returns: 'a The result of the input function call and prints to the stdout information that the function has been call with the given integer.

Iterative deepening.

Calls a function that accepts an input integer; and then calls it again with the integer incremented, if the previous call has failed.

f : int -> 'a: The input function.
n : int: The input integer.

Returns: 'a: The result of the input function call and prints to the stdout information that the function has been call with the given integer.

Example

 deepen id 1

val id: x: 'T -> 'T

Evaluates to 1 and prints stdout.

 Searching with depth limit 1

Full Usage: tab fm

Parameters:

fm : formula<fol> - The input formula

Returns: int The number of universal variables replaced, if the procedure succeeds, and prints to the stdout the depth limits (max number of universal variables to replace) tried.

Tests the validity of a formula with the tableau procedure.

fm : formula<fol>: The input formula

Returns: int: The number of universal variables replaced, if the procedure succeeds, and prints to the stdout the depth limits (max number of universal variables to replace) tried.

Example

 !! @"(forall x.
         P(a) /\ (P(x) ==> (exists y. P(y) /\ R(x,y))) ==>
         (exists z w. P(z) /\ R(x,w) /\ R(w,z))) <=>
         (forall x.
         (~P(a) \/ P(x) \/ (exists z w. P(z) /\ R(x,w) /\ R(w,z))) /\
         (~P(a) \/ ~(exists y. P(y) /\ R(x,y)) \/
         (exists z w. P(z) /\ R(x,w) /\ R(w,z))))"
 |> tab

Evaluates to 4 and prints to the stdout

 Searching with depth limit 0
 Searching with depth limit 1
 Searching with depth limit 2
 Searching with depth limit 3
 Searching with depth limit 4


                
                  
                    
                      tableau (fms, lits, n) cont (env, k)

Full Usage: tableau (fms, lits, n) cont (env, k)

Parameters:

fms : formula<fol> list - The set of DNF formulas (assumptions) to be refuted.

lits : formula<fol> list - The list of (derived) literals against which to refute the formulas.

n : int - The limit of universal variables to be replaced.

cont : func<string, term> * int -> func<string, term> * int - The supporting continuation function.

env : func<string, term> - The given instantiation under which trying refuting.

k : int - The counter of universal variables already replaced.

Returns: func<string, term> * int The pair of the successful instantiation together with the number of universal variables replaced, if the procedure succeeds.

Tries to refute a set of Skolem.askolemized formulas (assumptions) against a list of (derived) literals given a limit of universal variables to be replaced.

The procedure applies recursively the following rules. If the list is empty, fail: there are no refutations; otherwise consider the first formula.

If it is a conjunction, replace it with the two separated assumptions of its conjuncts;
if it is a disjunction, try to refute the first disjunct and 'update' the continuation function to 'remember' to try refute the second disjunct in case of failure;
if it is a universal formula, (i) replace it with its body with the universal variable replaced by a new fresh variable, (ii) move the original assumption at the end of the assumptions list, (iii) reduce the limit of universal variable that can be replaced and (iv) increment by one the counter of universal variables replaced;
if it is a literal, try to find a unifiable complement of it in the list of literals using the continuation function to iterate over each of them. If one complementary literal is found, return with the successful instantiation together with the number of universal variables replaced; otherwise, add the current formula to the list of literals and move on the next formula.

fms : formula<fol> list: The set of DNF formulas (assumptions) to be refuted.
lits : formula<fol> list: The list of (derived) literals against which to refute the formulas.
n : int: The limit of universal variables to be replaced.
cont : func<string, term> * int -> func<string, term> * int: The supporting continuation function.
env : func<string, term>: The given instantiation under which trying refuting.
k : int: The counter of universal variables already replaced.

Returns: func<string, term> * int: The pair of the successful instantiation together with the number of universal variables replaced, if the procedure succeeds.

Exception	Thrown with message `no proof at this level` when `n` < 0.
Exception	Thrown with message `tableau: no proof` when the list of input formulas `fms` is empty.

Example

 tableau ([!!"P(x)"], [!!"~P(f(y))"], 0) id (undefined, 0)
 |> fun (inst,nrInst) -> inst |> graph,nrInst

val id: x: 'T -> 'T

val inst: obj

val nrInst: obj

Evaluates to ([("x", ``f(y)``)], 0).

Example

 tableau ([!!"P(x)"], [!!"~P(f(y))"], -1) id (undefined, 0)
 |> fun (inst,nrInst) -> inst |> graph,nrInst

val id: x: 'T -> 'T

val inst: obj

val nrInst: obj

Throws System.Exception: no proof at this level.

Example

 tableau ([], [!!"~P(f(x))"], 0) id (undefined, 0)
 |> fun (inst,nrInst) -> inst |> graph,nrInst

val id: x: 'T -> 'T

val inst: obj

val nrInst: obj

Throws System.Exception: no proof.


                
                  
                    
                      tabrefute fms

Full Usage: tabrefute fms

Parameters:

fms : formula<fol> list - The input list of formulas.

Returns: int The number of universal variables replaced, if the procedure succeeds, and prints to the stdout the depth limits (max number of universal variables to replace) tried.

Tries to refute a set of Skolem.askolemized formulas using a iterative deepening of the Tableaux.tableau procedure.

fms : formula<fol> list: The input list of formulas.

Returns: int: The number of universal variables replaced, if the procedure succeeds, and prints to the stdout the depth limits (max number of universal variables to replace) tried.

Note

Crashes if the list of formulas is satisfiable or the search too long.

Example

 [!! "forall x y. P(x) /\ ~P(f(y))"; 
 !! "R(x,y) /\ ~R(x,y)"]
 |> tabrefute

Evaluates to 2 and prints to the stdout

 Searching with depth limit 0
 Searching with depth limit 1
 Searching with depth limit 2

Tableaux procedure optimized

Functions and values

Function or value Description

Function or value	Description
`splittab fm` Full Usage: `splittab fm` Parameters: fm : `formula<fol>` - The input formula Returns: `int list` The numbers of universal variables replaced for each of the independently tested subproblems, if the procedure succeeds, and prints to the `stdout` the depth limits (max number of universal variables to replace) tried.	Tests the validity of a formula splitting in subproblems and testing each of them with the tableau procedure. The formula is generalized, negated and askolemized. Then Prop.simpdnf is applied and, thus, the formula transformed in a sort of a 'DNF set of clauses' with possibly some universal formulas in place of literals. Each of these 'clauses' is tested separately with Tableaux.tabrefute. fm : `formula<fol>` The input formula Returns: `int list` The numbers of universal variables replaced for each of the independently tested subproblems, if the procedure succeeds, and prints to the `stdout` the depth limits (max number of universal variables to replace) tried. Example `!!"((exists x. forall y. P(x) <=> P(y)) <=> ((exists x. Q(x)) <=> (forall y. Q(y)))) <=> ((exists x. forall y. Q(x) <=> Q(y)) <=> ((exists x. P(x)) <=> (forall y. P(y))))" \|> splittab` Evaluates to `[5; 4; 5; 3; 3; 3; 2; 4; 6; 2; 3; 3; 4; 3; 3; 3; 3; 2; 2; 3; 6; 3; 2; 4; 3; 3; 3; 3; 3; 4; 4; 4]` and prints to the `stdout` `Searching with depth limit 0 Searching with depth limit 1 Searching with depth limit 2 ... Searching with depth limit 0 Searching with depth limit 1 ...`


                
                  
                    
                      splittab fm

Full Usage: splittab fm

Parameters:

fm : formula<fol> - The input formula

Returns: int list The numbers of universal variables replaced for each of the independently tested subproblems, if the procedure succeeds, and prints to the stdout the depth limits (max number of universal variables to replace) tried.

Tests the validity of a formula splitting in subproblems and testing each of them with the tableau procedure.

The formula is generalized, negated and askolemized. Then Prop.simpdnf is applied and, thus, the formula transformed in a sort of a 'DNF set of clauses' with possibly some universal formulas in place of literals. Each of these 'clauses' is tested separately with Tableaux.tabrefute.

fm : formula<fol>: The input formula

Returns: int list: The numbers of universal variables replaced for each of the independently tested subproblems, if the procedure succeeds, and prints to the stdout the depth limits (max number of universal variables to replace) tried.

Example

 !!"((exists x. forall y. P(x) <=> P(y)) <=>
     ((exists x. Q(x)) <=> (forall y. Q(y)))) <=>
    ((exists x. forall y. Q(x) <=> Q(y)) <=>
     ((exists x. P(x)) <=> (forall y. P(y))))"
 |> splittab

Evaluates to [5; 4; 5; 3; 3; 3; 2; 4; 6; 2; 3; 3; 4; 3; 3; 3; 3; 2; 2; 3; 6; 3; 2; 4; 3; 3; 3; 3; 3; 4; 4; 4] and prints to the stdout

 Searching with depth limit 0
 Searching with depth limit 1
 Searching with depth limit 2
 ...
 Searching with depth limit 0
 Searching with depth limit 1
 ...

Calculemus

Tableaux Module

Table of contents

Unification of literals

Functions and values

Example

Example

Example

Example

Example

Example

Example

Example

Example

Refutation via unification

Functions and values

Example

Example

Prawitz procedure

Functions and values

Example

Example

Tableaux procedure

Functions and values

Example

Example

Example

Example

Example

Note

Example

Tableaux procedure optimized

Functions and values

Example