Calculemus

Paramodulation Module

Namespace: Calculemus
Assembly: Calculemus.dll

Paramodulation.

Functions and values

Function or value Description

overlapc (l, r) cl rfn acc

Full Usage: overlapc (l, r) cl rfn acc

Parameters:
    l : term - The LHS of the input equation.
    r : term - The RHS of the input equation.
    cl : formula<fol> list - The input literal.
    rfn : func<string, term> -> formula<fol> list -> 'a - The function that applied to the resulting instantiation gives the critical pair arising from that overlap.
    acc : 'a list

Returns: 'a list All possibile overlaps of the equation l = r with fm.

Finds all possibile 'overlaps' of an equation with a clause.

l : term

The LHS of the input equation.

r : term

The RHS of the input equation.

cl : formula<fol> list

The input literal.

rfn : func<string, term> -> formula<fol> list -> 'a

The function that applied to the resulting instantiation gives the critical pair arising from that overlap.

acc : 'a list
Returns: 'a list

All possibile overlaps of the equation l = r with fm.

overlapl (l, r) fm rfn

Full Usage: overlapl (l, r) fm rfn

Parameters:
    l : term - The LHS of the input equation.
    r : term - The RHS of the input equation.
    fm : formula<fol> - The input literal.
    rfn : func<string, term> -> formula<fol> -> 'a - The function that applied to the resulting instantiation gives the critical pair arising from that overlap.

Returns: 'a list All possibile overlaps of the equation l = r with fm.

Finds all possibile 'overlaps' of an equation with a literal.

l : term

The LHS of the input equation.

r : term

The RHS of the input equation.

fm : formula<fol>

The input literal.

rfn : func<string, term> -> formula<fol> -> 'a

The function that applied to the resulting instantiation gives the critical pair arising from that overlap.

Returns: 'a list

All possibile overlaps of the equation l = r with fm.

para_clauses cls1 cls2

Full Usage: para_clauses cls1 cls2

Parameters:
    cls1 : formula<fol> list - The first input clause.
    cls2 : formula<fol> list - The second input clause.

Returns: formula<fol> list list All the paramodulants between the two clauses.

Performs paramodulation of each clause within the other.

cls1 : formula<fol> list

The first input clause.

cls2 : formula<fol> list

The second input clause.

Returns: formula<fol> list list

All the paramodulants between the two clauses.

paraloop (used, unused)

Full Usage: paraloop (used, unused)

Parameters:
    used : formula<fol> list list - The working list of clauses, initially empty.
    unused : formula<fol> list list - The input list of clauses to be refuted.

Returns: bool true, if a refutation with paramodulation for unused is found.

Resolution loop with paramodulation.

used : formula<fol> list list

The working list of clauses, initially empty.

unused : formula<fol> list list

The input list of clauses to be refuted.

Returns: bool

true, if a refutation with paramodulation for unused is found.

Exception Thrown with message No proof found when no refutation could be found.
Note

Prints diagnostic informations to the stdout

paramodulate pcl ocl

Full Usage: paramodulate pcl ocl

Parameters:
    pcl : formula<fol> list - The paramodulating clause.
    ocl : formula<fol> list - The clause to which paramodulation is applied.

Returns: formula<fol> list list The list of clauses resulting from the paramodulation.

Applies paramodulation to a clause ocl using all the positive equations in a paramodulating clause pcl.

Paramodulation is the following inference rule, where \(s = t\) may be either \(s = t\) or \(t = s\): \[ \dfrac {C \lor s = t \quad D \lor P[s']} {\text{subst}\ \sigma\ (C \lor D \lor P[t])} \]

pcl : formula<fol> list

The paramodulating clause.

ocl : formula<fol> list

The clause to which paramodulation is applied.

Returns: formula<fol> list list

The list of clauses resulting from the paramodulation.

Example 

 paramodulate !!>["C";"S(0) = 1"] !!>["P(S(x))";"D"]
Evaluates to [[`C`; `D`; `P(1)`]].

paramodulation fm

Full Usage: paramodulation fm

Parameters:
Returns: bool list The list of the results of Paramodulation.pure_paramodulation on each subproblems, if the formula is valid and a proof could be found.

Tests the validity of a formula splitting it in subproblems and then testing them with a resolution procedure with paramodulation.

fm : formula<fol>

The input formula.

Returns: bool list

The list of the results of Paramodulation.pure_paramodulation on each subproblems, if the formula is valid and a proof could be found.

Exception Thrown with message No proof found when no proof could be found.
Note

Prints diagnostic informations to the stdout.

Example 

 !! @"(forall x. f(f(x)) = f(x)) /\ (forall x. exists y. f(y) = x)
     ==> forall x. f(x) = x"
 |> paramodulation
Evaluates to [true] and prints to the stdout: 
 0 used; 4 unused.
 1 used; 3 unused.
 2 used; 4 unused.
 3 used; 8 unused.
 4 used; 11 unused.
 5 used; 13 unused.
 6 used; 21 unused.
 7 used; 40 unused.
 8 used; 64 unused.
 9 used; 83 unused.
 10 used; 108 unused.
 11 used; 125 unused.

pure_paramodulation fm

Full Usage: pure_paramodulation fm

Parameters:
Returns: bool true, if the input formula is unsatisfiable and a refutation could be found.

Tests the unsatisfiability of a formula using a resolution with paramodulation.

fm : formula<fol>

The input formula.

Returns: bool

true, if the input formula is unsatisfiable and a refutation could be found.

Exception Thrown with message No proof found when no refutation could be found (and this is always the case if the formula is either valid or satisfiable).
Note

Prints diagnostic informations to the stdout.