Calculemus

Resolution Module

Namespace: Calculemus
Assembly: Calculemus.dll

Resolution.

Table of contents

Unification of literals

Functions and values

Function or value Description

mgu l env

Full Usage: mgu l env

Parameters:
    l : formula<fol> list - The input list 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.

Returns: func<string, term> An MGU, if the unification is possible and there are no cycles.

Returns an MGU for a set of literals.

The difference with Tableaux.unify_literals is that this function can be applied to a list of literals instead of a pair and also that it returns an MGU and not a simple unifier.

l : formula<fol> list

The input list 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.

Returns: func<string, term>

An MGU, 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
Note

See also Tableaux.unify_literals, Unif.solve

Example

Successful unification 

 mgu !!>["P(x)";"P(f(y))"] undefined
 |> graph
Evaluates to [("x", ``f(y)``)].

Example

Degenerated case 

 mgu !!>["false";"false"] undefined
 |> graph
Evaluates to [].

Example

Cyclic assignment 

 mgu !!>["P(x)";"P(f(x))"] undefined
Throws System.Exception: cyclic.

Example

Impossible unification 

 mgu !!>["P(0)";"P(f(y))"] undefined
Throws System.Exception: impossible unification.

Example

Invalid input 

 mgu !!>["P(x) /\ Q(x)";"P(f(y)) /\ Q(f(y))"] undefined
Throws System.Exception: Can't unify literals.

unifiable p q

Full Usage: unifiable p q

Parameters:
Returns: bool true, if the input are literals and unifiable; otherwise, false.

Tests if two literals are unifiable.

p : formula<fol>

The first input literal.

q : formula<fol>

The second input literal.

Returns: bool

true, if the input are literals and unifiable; otherwise, false.

Example 

 unifiable !!"P(x)" !!"P(f(y))"
Evaluates to true.

Example 

 unifiable !!"P(x)" !!"P(f(x))"
Evaluates to false.

Basic resolution

Functions and values

Function or value Description

basic_resloop (used, unused)

Full Usage: basic_resloop (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 for unused is found.

Basic resolution loop.

Keeps generating resolvents till the empty clause is derived.

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 for unused is found.

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

Prints diagnostic informations to the stdout.

Example 

 basic_resloop ([],!!>>[["P(x)"];["~P(x)"]])
Evaluates to true and prints to the stdout
 0 used; 2 unused.
 1 used; 1 unused.

Example 

 basic_resloop ([],!!>>[["P(x)"]])
Throws System.Exception: No proof found.

basic_resolution fm

Full Usage: basic_resolution fm

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

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

fm : formula<fol>

The input formula.

Returns: bool list

The list of the results of Resolution.pure_basic_resolution 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

Valid formula (example from Davis and Putnam (1960)) 

 !! @"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)))"
 |> basic_resolution
Evaluates to [true] and prints to the stdout: 
 0 used; 3 unused.
 1 used; 2 unused.
 ...
 82 used; 478 unused.
 83 used; 483 unused.
 84 used; 488 unused.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> basic_resolution
Throws System.Exception: No proof found.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> basic_resolution
Throws System.Exception: No proof found.

pure_basic_resolution fm

Full Usage: pure_basic_resolution fm

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

Tests the unsatisfiability of a formula using the basic resolution procedure.

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.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> pure_basic_resolution
Evaluates to true and prints to the stdout: 
 0 used; 2 unused.
 1 used; 1 unused.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> pure_basic_resolution
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

Example

Valid formula 

 !!"""P(x) \/ ~P(x)"""
 |> pure_basic_resolution
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

rename pfx cls

Full Usage: rename pfx cls

Parameters:
    pfx : string - The first input literal.
    cls : formula<fol> list - The list of formulas.

Returns: formula<fol> list The list of formulas with the free variables with the given prefix.

Renames the free variables in a list of formulas by adding the given prefix.

pfx : string

The first input literal.

cls : formula<fol> list

The list of formulas.

Returns: formula<fol> list

The list of formulas with the free variables with the given prefix.

Example 

 rename "old_" !!>["P(x)";"Q(y)"]
Evaluates to [`P(old_x)`; `Q(old_y)`].

resolve_clauses cls1 cls2

Full Usage: resolve_clauses cls1 cls2

Parameters:
Returns: formula<fol> list list All the resolvents of cl1 and cl2.

Returns all resolvents of two clauses.

cls1 : formula<fol> list
cls2 : formula<fol> list
Returns: formula<fol> list list

All the resolvents of cl1 and cl2.

Example 

 resolve_clauses 
   !!>["P(x)";"Q(x)";"P(0)"]
   !!>["~P(f(y))";"~P(z)";"~Q(z)"]
Evaluates to 
 [[`P(0)`; `Q(yz)`; `~P(f(yy))`; `~Q(yz)`];
  [`P(0)`; `Q(f(yy))`; `~P(yz)`; `~Q(yz)`];
  [`P(0)`; `Q(f(yy))`; `~Q(f(yy))`];
  [`Q(0)`; `~P(f(yy))`; `~Q(0)`];
  [`P(yz)`; `P(0)`; `~P(yz)`; `~P(f(yy))`];
  [`P(xx)`; `Q(xx)`; `~P(f(yy))`; `~Q(0)`];
  [`Q(0)`; `~P(f(yy))`; `~Q(0)`]]

resolvents cl1 cl2 p acc

Full Usage: resolvents cl1 cl2 p acc

Parameters:
Returns: formula<fol> list list The result of resolving cl1 and cl2 on the literal p.

Returns all resolvents of two clauses on a given literal.

cl1 : formula<fol> list

The first input clause.

cl2 : formula<fol> list

The second input clause.

p : formula<fol>

The given literal.

acc : formula<fol> list list

The supporting accumulator.

Returns: formula<fol> list list

The result of resolving cl1 and cl2 on the literal p.

Example 

 resolvents 
   !!>["P(x)";"~R(x,y)";"Q(x)";"P(0)"]
   !!>["~P(f(y))";"T(x,y,z)";"~P(z)"]
   !!"P(x)"
   []
Evaluates to 
 [[`P(0)`; `Q(z)`; `T(z,y,z)`; `~P(f(y))`; `~R(z,y)`];
  [`P(0)`; `Q(f(y))`; `T(f(y),y,z)`; `~P(z)`; `~R(f(y),y)`];
  [`P(0)`; `Q(f(y))`; `T(f(y),y,f(y))`; `~R(f(y),y)`];
  [`Q(0)`; `T(0,y,0)`; `~P(f(y))`; `~R(0,y)`]]

Matching

Functions and values

Function or value Description

match_literals env (p, q)

Full Usage: match_literals 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 resulting matching, if there is.

Returns the matchings of a pair of literals.

Matching is a cut-down version of unification in which the instantiation of variables is allowed only in the first term.

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 resulting matching, if there is.

Exception Thrown with message term_match when there are no matchings.
Exception Thrown with message match_literals when there input formulas are not literals.
Example 

 (!!"P(x)",!!"P(f(y))")
 |> match_literals undefined
 |> graph
Evaluates to [("x", ``f(y)``)].

Example 

 (!!"P(f(y))",!!"P(x)")
 |> match_literals undefined
Throws System.Exception: term_match.

Example 

 (!!"P(x) /\ Q(x)",!!"P(f(y)) /\ Q(f(y))")
 |> match_literals undefined
Throws System.Exception: match_literals.

term_match env eqs

Full Usage: term_match env eqs

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.
    eqs : (term * term) list - The input list of term-term pairs to be matched.

Returns: func<string, term> The resulting matchings, if there are.

Returns the matchings of a list of term-term pairs.

Matching is a cut-down version of unification in which the instantiation of variables is allowed only in the first term.

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.

eqs : (term * term) list

The input list of term-term pairs to be matched.

Returns: func<string, term>

The resulting matchings, if there are.

Exception Thrown with message term_match when there are no matchings.
Example 

 [!!!"x",!!!"f(y)"]
 |> term_match undefined
 |> graph
Evaluates to [("x", ``f(y)``)].

Example 

 [!!!"f(y)",!!!"x"]
 |> term_match undefined
Throws System.Exception: term_match.

Subsumption

Functions and values

Function or value Description

incorporate gcl cl unused

Full Usage: incorporate gcl cl unused

Parameters:
    gcl : formula<fol> list - The given clause.
    cl : formula<fol> list - The clause to be inserted after checking.
    unused : formula<fol> list list - The input list fo clauses.

Returns: formula<fol> list list The input list unused incremented by cl, if this latter passes the check; otherwise, the input list unused unchanged.

Inserts a newly generated clause cl by first removing the tautological and replacing the subsumed ones.

gcl : formula<fol> list

The given clause.

cl : formula<fol> list

The clause to be inserted after checking.

unused : formula<fol> list list

The input list fo clauses.

Returns: formula<fol> list list

The input list unused incremented by cl, if this latter passes the check; otherwise, the input list unused unchanged.

Example

Inserted since neither tautological nor subsumed 

 !!>>[["P(x)"];["Q(y)"]]
 |> incorporate [!!"R(0)"] [!!"R(f(z))"]
Evaluates to [[`P(x)`]; [`Q(y)`]; [`R(f(z))`]].

Example

Not inserted since subsumed by gcl 

 !!>>[["P(x)"];["Q(y)"]]
 |> incorporate [!!"R(w)"] [!!"R(f(z))"]
Evaluates to [[`P(x)`]; [`Q(y)`]].

Example

Not inserted since subsumed by another clause in the list 

 !!>>[["P(x)"];["Q(y)"]]
 |> incorporate [!!"R(0)"] [!!"P(f(z))"]
Evaluates to [[`P(x)`]; [`Q(y)`]].

Example

Not inserted since tautological 

 !!>>[["P(x)"];["Q(y)"]]
 |> incorporate [!!"R(0)"] !!>["R(f(z))";"~R(f(z))"]
Evaluates to [[`P(x)`]; [`Q(y)`]].

replace cl lis

Full Usage: replace cl lis

Parameters:
    cl : formula<fol> list - The clause that could subsume.
    lis : formula<fol> list list - The input list of clauses.

Returns: formula<fol> list list The list obtained by lis replacing with cl each of its element that are subsumed by it.

Replaces each clause in a list with the given one, if the latter subsumes the first.

cl : formula<fol> list

The clause that could subsume.

lis : formula<fol> list list

The input list of clauses.

Returns: formula<fol> list list

The list obtained by lis replacing with cl each of its element that are subsumed by it.

Example 

 !!>>[["Q(0)";"P(f(y))"];["P(x)";"~P(x)"]]
 |> replace !!>["P(x)"]
Evaluates to [[`P(x)`]; [`P(x)`; `~P(x)`]].

subsumes_clause cls1 cls2

Full Usage: subsumes_clause cls1 cls2

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

Returns: bool true, if the first clause subsumes the second; otherwise, false.

Tests if the first clause subsumes the second.

cls1 : formula<fol> list

The first input clause.

cls2 : formula<fol> list

The second input clause.

Returns: bool

true, if the first clause subsumes the second; otherwise, false.

Example 

 subsumes_clause !!>["P(x)"] !!>["Q(0)";"P(f(y))"]
Evaluates to true.

Example 

 subsumes_clause !!>["Q(0)";"P(f(y))"] !!>["P(x)"]
Evaluates to false.

Resolution with subsumption and replacement

Functions and values

Function or value Description

pure_resolution_wsubs fm

Full Usage: pure_resolution_wsubs 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 subsumption and replacement.

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.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> pure_resolution_wsubs
Evaluates to true and prints to the stdout: 
 0 used; 2 unused.
 1 used; 1 unused.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> pure_resolution_wsubs
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

Example

Valid formula 

 !!"""P(x) \/ ~P(x)"""
 |> pure_resolution_wsubs
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

resloop_wsubs (used, unused)

Full Usage: resloop_wsubs (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 for unused is found.

Resolution loop with subsumption and replacement.

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 for unused is found.

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

Prints diagnostic informations to the stdout

Example 

 resloop_wsubs ([],!!>>[["P(x)"];["~P(x)"]])
Evaluates to true and prints to the stdout
 0 used; 2 unused.
 1 used; 1 unused.

Example 

 resloop_wsubs ([],!!>>[["P(x)"]])
Throws System.Exception: No proof found.

resolution_wsubs fm

Full Usage: resolution_wsubs fm

Parameters:
Returns: bool list The list of the results of Resolution.pure_resolution_wsubs 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 that handles subsumption and replacement.

fm : formula<fol>

The input formula.

Returns: bool list

The list of the results of Resolution.pure_resolution_wsubs 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

Valid formula (example from Davis and Putnam (1960)) 

 !! @"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)))"
 |> resolution_wsubs
Evaluates to [true] and prints to the stdout: 
 ...
 6 used; 3 unused.
 7 used; 2 unused.
Note how much the number of clauses generated has been reduced compared to Resolution.basic_resolution.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> resolution_wsubs
Throws System.Exception: No proof found.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> resolution_wsubs
Throws System.Exception: No proof found.

Positive resolution

Functions and values

Function or value Description

presloop (used, unused)

Full Usage: presloop (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 for unused is found.

Positive resolution loop.

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 for unused is found.

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

Prints diagnostic informations to the stdout

Example 

 presloop ([],!!>>[["P(x)"];["~P(x)"]])
Evaluates to true and prints to the stdout
 0 used; 2 unused.
 1 used; 1 unused.

Example 

 presloop ([],!!>>[["P(x)"]])
Throws System.Exception: No proof found.

presolution fm

Full Usage: presolution fm

Parameters:
Returns: bool list The list of the results of Resolution.pure_presolution 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 the positive resolution procedure.

fm : formula<fol>

The input formula.

Returns: bool list

The list of the results of Resolution.pure_presolution 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

Valid formula (Łoś example) 

 !! @"(forall x y z. P(x,y) /\ P(y,z) ==> P(x,z)) /\
      (forall x y z. Q(x,y) /\ Q(y,z) ==> Q(x,z)) /\
      (forall x y. Q(x,y) ==> Q(y,x)) /\
      (forall x y. P(x,y) \/ Q(x,y))
      ==> (forall x y. P(x,y)) \/ (forall x y. Q(x,y))"
 |> presolution
Evaluates to [true] and prints to the stdout: 
 0 used; 6 unused.
 1 used; 5 unused.
 ...
 34 used; 42 unused.
 35 used; 41 unused.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> presolution
Throws System.Exception: No proof found.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> presolution
Throws System.Exception: No proof found.

presolve_clauses cls1 cls2

Full Usage: presolve_clauses cls1 cls2

Parameters:
Returns: formula<fol> list list All the resolvents of cl1 and cl2, if at least one of them is completely positive; otherwise, an empty list.

Returns all resolvents of two clauses if at least one of them contains only positive literals.

cls1 : formula<fol> list
cls2 : formula<fol> list
Returns: formula<fol> list list

All the resolvents of cl1 and cl2, if at least one of them is completely positive; otherwise, an empty list.

Example 

 presolve_clauses 
   !!>["P(x)";"Q(x)";"P(0)"]
   !!>["~P(f(y))";"~P(z)";"~Q(z)"]
Evaluates to 
 [[`P(0)`; `Q(yz)`; `~P(f(yy))`; `~Q(yz)`];
  [`P(0)`; `Q(f(yy))`; `~P(yz)`; `~Q(yz)`];
  [`P(0)`; `Q(f(yy))`; `~Q(f(yy))`];
  [`Q(0)`; `~P(f(yy))`; `~Q(0)`];
  [`P(yz)`; `P(0)`; `~P(yz)`; `~P(f(yy))`];
  [`P(xx)`; `Q(xx)`; `~P(f(yy))`; `~Q(0)`];
  [`Q(0)`; `~P(f(yy))`; `~Q(0)`]]

Example 

 presolve_clauses 
   !!>["P(x)";"Q(x)";"P(0)";"~A"]
   !!>["~P(f(y))";"~P(z)";"~Q(z)"]
Evaluates to [].

pure_presolution fm

Full Usage: pure_presolution 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 positive resolution procedure.

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.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> pure_presolution
Evaluates to true and prints to the stdout: 
 0 used; 2 unused.
 1 used; 1 unused.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> pure_presolution
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

Example

Valid formula 

 !!"""P(x) \/ ~P(x)"""
 |> pure_presolution
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

Set-of-support restriction

Functions and values

Function or value Description

pure_resolution_wsos fm

Full Usage: pure_resolution_wsos 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 procedure with subsumption and replacement and the set-of-support restriction.

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.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> pure_resolution_wsos
Evaluates to true and prints to the stdout: 
 0 used; 2 unused.
 1 used; 1 unused.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> pure_resolution_wsos
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

Example

Valid formula 

 !!"""P(x) \/ ~P(x)"""
 |> pure_resolution_wsos
Throws System.Exception: No proof found and prints to the stdout: 
 0 used; 1 unused.

resolution_wsos fm

Full Usage: resolution_wsos fm

Parameters:
Returns: bool list The list of the results of Resolution.pure_resolution_wsos 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 using a resolution procedure with subsumption and replacement and the set-of-support restriction.

fm : formula<fol>

The input formula.

Returns: bool list

The list of the results of Resolution.pure_resolution_wsos 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

Valid formula (Łoś 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)))"
 |> resolution_wsos
Evaluates to [true] and prints to the stdout: 
 0 used; 6 unused.
 1 used; 5 unused.
 ...
 34 used; 42 unused.
 35 used; 41 unused.

Example

Satisfiable (not valid) formula 

 !!"P(x)"
 |> resolution_wsos
Throws System.Exception: No proof found.

Example

Unsatisfiable formula 

 !!"P(x) /\ ~P(x)"
 |> resolution_wsos
Throws System.Exception: No proof found.