Resolution for Beginners

A Resolution Theorem Prover for the Propositional Calculus

Nigel Seel, Interweave Consulting, Wells, Somerset, UK.               Version 1.0,  July 27^th 2013

The Python 3 code is here.

Introduction

The core of intelligence is ‘Generate and Test’:

(1) Generate a way of thinking about the world, a new paradigm if you wish, which we encode as axioms for a ‘theory’;

(2) Test the new theory by deducing its consequences and see if they stack up in the real world.

The ‘test’ part requires a theorem prover (in some guise) and that’s what we’re going to build here.

A theorem prover has three main components:

1. A knowledge base and something to prove – a goal.

2. An inference mechanism to draw conclusions from premises in the knowledge base.

3. A control mechanism to guide the inferences towards the goal.

For maximum clarity we’re operating in the propositional calculus here, so we’re just dealing with sentence letters and their negations. This is quite enough to solve not-entirely-trivial problems. The control mechanism used (‘set of support’) is quite robust and can be used for more powerful logics. The implementation code is in Python 3 and is copied across from my Eclipse IDE: the run data is taken also from Eclipse. The theorem prover code is written for maximum clarity and minimal operational efficiency: it proves you can write LISP in any (sufficiently powerful) language!

In Part 1 we discuss the resolution rule in detail and solve a simple puzzle by a formal resolution proof. In Part 2 I provide the annotated code of the theorem prover. In Part 3 we look at test data from the puzzle and elsewhere and in Part 4 the results of running the code, i.e. the actual proofs.

You can run the code yourself by deleting (or commenting out) the descriptive material or by grabbing it directly from here. Remember, it’s Python 3.

Part 1. The Resolution Rule

Consider the following puzzle.

“If the unicorn is mythical then it is immortal, but if it is not mythical then it is a mortal mammal. If the unicorn is either immortal or a mammal, then it is horned. The unicorn is magical if it is horned.”

[“Artificial Intelligence, A Modern Approach”, Russell and Norvig, 1995, section 6.6 Ex. 6.5 (p.181)].

We are asked to consider: is the unicorn mythical? Is it magical? Is it horned?

Given the obscuration of the puzzle the answers are obvious, but only after a few minutes concentration J. 

Here is how a computer resolution theorem prover would manage it. We start by changing the English statements into propositions.

• U = “The unicorn is mythical”
• I = “The unicorn is immortal”
• M = “The unicorn is a mortal mammal”
• H = “The unicorn is horned”
• T = “The unicorn is magical” (after thaumaturgy).

Now the puzzle can be restated in propositional calculus as four sentences:

1. U -> I
2. –U -> M
3. I or M -> H
4. H -> T

And we’re asked: U? T? H?

The four sentences above are implicitly ‘and’ed together. Unfortunately we can’t use the resolution rule immediately as the format of the sentences is wrong - we need to rewrite each sentence in ‘normal form’, using only ‘not’ and ‘or’. And then use set notation to group the literals which are ‘or’ed together.

Here is how we do the transformation into ‘normal form’:

• P -> Q is equivalent to –P or Q … which we write as {-P, Q};
• P or Q -> R ... is equivalent to
• -(P or Q) or R … which is
• (-P and –Q) or R … by De Morgan’s law, which is
• (-P or R) and (-Q or R) … by distributivity (ending up as two clauses {-P, R} {-Q, R}).

1.1 Some Notation

Atomic sentences are TRUE, FALSE and symbols such as P, Q, R which stand for propositions.

A literal is either an atomic sentence or its negation:  so P is a literal and so is –P.

A clause is a set of literals which are ‘or’ed together – it’s what we’ve written in set brackets above.

A resolution theorem prover works on a set of clauses which are implicitly ‘and’ed together. This format of the problem statement is called conjunctive normal form (CNF). So that’s the jargon finished with, back to the problem.

Applying these ideas to our puzzle we get:

1. {-U, I}
2. {U, M}
3. {-I, H}
4. {-M, H}
5. {-H, T}.

Now for the resolution rule: this tells us that if we have

{P, Q} and {-P, R}

we can ‘cancel’ the P, -P pair and conclude

 {Q, R}.

The intuition is that either P is true or false: if P is false then Q must be true and if P is true (so -P false) then R must be true. So either way, either Q or R is true hence {Q, R}.

Let’s apply resolution to our puzzle, using the line numbers to keep track.

6. {-U, I} resolves with {U, M} to give {I, M}   (1 and 2)

7. {I, M} resolves with {-I, H} to give {M, H}   (6 and 3)

8. {M, H} resolves with {-M, H} to give {H}   (7 and 4)

So we conclude that the unicorn is horned.

In a proper resolution system we would have added the extra clause {-H} as the negation of the conclusion for a proof by contradiction: {H} resolves with {-H} to give {} – the empty clause – which is taken to be FALSE. So H must be true as its negation leads to a contradiction.

A similar series of steps lead to a proof of T, that the unicorn is magical (resolve {H} with 5). But sadly, one cannot prove that the unicorn is mythical!

---

Part 2: Building a Propositional Calculus Resolution Theorem Prover in Python

'''

Created on 27 Jul 2013

@author: Nigel Seel

A Resolution Theorem Prover for Propositional  Calculus

'''

We’re going to look at the theorem prover code bottom-up, starting with simple helper procedures.

2.1. complementary

def complementary(l1, l2):

    ''' receives two literals and returns TRUE if they are complementary.

    So complementary('P', '-P') = TRUE and complementary('P','Q') = FALSE.

    '''

    return (l1[0] == '-' and l1[1:] == l2) or (l2[0] == '-' and l2[1:] == l1)

Here’s what’s going on. If c1 and c2 are clauses

c1 = ['P', 'Q', '-R', 'S']

c2 = ['-S', 'P', 'R']

we can successfully resolve on both R and S. This depends on us recognising that ‘S’ and ‘-S’, and ‘R’ and ‘-R’ are complementary literals - and that’s what complementary(l1, l2) does. It takes as input two literals and returns TRUE if they’re complementary, otherwise FALSE.

2.2 deletefromclause

def deletefromclause(clause,l1,l2):

    ''' deletes literals l1 and l2 from clause leaving the remaining literals.

    '''

    newclause = []

    for lit in clause:

        if lit != l1 and lit != l2:

            newclause = newclause + [lit]

    return newclause

If, for example, we resolve c1 and c2 above on ‘R’ we get the new clause c3 = [‘P’, ‘Q’, ‘S’, ‘-S’, ‘P’] which is the union of c1 and c2 with the complementary literals we’re resolving on (‘R’ and ‘-R’) deleted. That’s how resolution works. So we need a procedure to join the two parent clauses together and then delete the complementary literals.

Below, we’re going to invoke it like this:

newclause = deletefromclause(c1 + c2,l1,l2)        where l1 =’ R’ and l2 = ‘-R’.

2.3 dedup

You will have noticed that the resolvant of c1 and c2 above contains two instances of ‘P’ - which clogs the inference engine. We therefore remove duplicates in a list by using dedup(licate).

def dedup(lst):

    ''' removes duplicate elements from list '''

    if lst == []:

        return []

    first,*rest = lst

    if first in rest:

        return dedup(rest)

    else:

        return [first] + dedup(rest)

2.4 resolve

def resolve(c1, c2):

    ''' resolves clauses c1 and c2 together on any matching literals and returns a list of the resolvant clauses. So if c1 = ['P', 'Q', '-R', 'S'] and c2 = [ '-S', 'P', 'R'] then

resolve(c1, c2) =   [['P', 'Q', 'S', '-S', 'P'], ['P', 'Q', '-R', 'P', 'R']]

   '''

    clauses = []

    for l1 in c1:

        for l2 in c2:

            if complementary(l1, l2):

                newclause = deletefromclause(c1 + c2,l1,l2)

                newclause = dedup(newclause)

                clauses = clauses + [newclause]

    return clauses

This is the central magic of the theorem prover.  Resolve will take two clauses and produce a list of lists – all the resolvant clauses as shown in its self-documentation above. Notice that in this simple version we’re not keeping track of the clauses used (they’re not numbered) nor the literal resolved upon to produce each resolvant. If you want to output proofs you can read and understand, these need to be added.

'''  --- Test Data ---

c1 = ['P', 'Q', '-R', 'S']

c2 = ['-S', 'P', 'R']

               

print(resolve(c1,c2))

'''

2.5 The resolution procedure

So we have a collection of clauses and a procedure – resolve – which can resolve any two together to return a further collection of resolvant clauses. How should we proceed?

Applying resolve at random will just produce an ever-growing tree of pointless consequences. Instead we focus on the goal statement. Since we’re trying to prove it (by contradiction) we start by resolving the goal-sentence (in its negated form) against the knowledge base (Base) to see if we can get a contradiction (the empty clause). Most likely we’ll just get some new resolvants which are logically connected with the goal. The original goal + any resolvants resulting from it, is called the ‘set of support’. We make sure going forwards that at least one of the inputs into every resolution step comes from the set of support and put the resolution outputs back into the set of support. This ensures we keep goal-focussed.

The exact mechanism is three steps (starting with the original base set of clauses + original negated goal.

1. We choose a good (as short as possible) candidate clause from the set of support – initially just the negated goal statement - and resolve it against every clause in the base. We also remove that candidate from the current set of support.

2. We append the resulting list of resolvant clauses both to the set of support and the base.

3. We go back to 1.

If one of the resolvants is the empty list we have a proof; if the set of support is empty (i.e. nothing left to resolve with) we have to stop and admit there is no proof.

Note that the strategy of sorting the set of support clauses by length so that unit clauses (literals) come first is known as unit preference. Clearly if you have ‘P’ in the set of support and ‘-P’ in the base then you want to resolve these two as soon as possible.

2.6 collectNewResolvants

The procedure collectNewResolvants is very simple. It just takes the chosen clause from the set of support – SoSclause – and resolves it against every clause in the current base. The result is a list of clauses, the resolvants, which it hands back to the top-level theorem prover as newResolvants. Recall that resolve produces a list of clauses – a list of lists.

def collectNewResolvants(Base, SoSclause):

    newResolvants = []

    for clause in Base:

        newResolvants = newResolvants + resolve(clause,SoSclause)

    return newResolvants

2.7 PCRTP

This is the top level of the theorem prover.

def PCRTP(Base, SoS, i):

    print('Iteration', i)

    print('Current Base = ', Base)

    print('Current SoS = ', SoS)

    if SoS == []:

        print('SoS empty  - cannot be proved')

    else:

        print('Current SoS clause = ', SoS[0])

        newResolvants = collectNewResolvants(Base, SoS[0])

        if [] in newResolvants:

            print('New Resolvants = ', newResolvants)

            print('empty clause found - proved')

        else:

            Base = Base + newResolvants

            SoS = sorted(dedup(SoS[1:] + newResolvants),key=len)

            print('New Resolvants = ', newResolvants)

            print('New Base = ', Base)

            print('New SoS = ', SoS)

            print('---')

            PCRTP(Base, SoS, i + 1)

Here at last is the top-level ‘Propositional Calculus Resolution Theorem Prover’. It implements the procedure described at the beginning of this section. Most of the code consists of print statements so you get a very clear idea as to what’s going on at runtime (data below).

PCRTP is called with the current base and set of support, which it prints. It first checks to see if the SoS is empty. If there is nothing there, no further work can be done and we terminate without a proof.

If SoS is not empty we print it and then collect all the resolvants of the first entry of SoS together with the base. We look at the results. If the empty clause is there, we have a proof and we terminate.

Otherwise we have to keep going: we add the new resolvants both to the base and to the rest of the set of support (deleting the preferred first entry we’ve just used), remove duplicates and sort the set of support on clause length (unit preference). Then we do some more printing to show what’s going on and re-enter the procedure at the next iteration.

So there we have it: a resolution theorem prover demystified! Time to look at the test data and check the results.

2.8 Further Reading

“Artificial Intelligence – Resolution for Propositional Calculus” by Lila Kari, University of Western Ontario.  http://www.csd.uwo.ca/~lila/logic/ai.pdf .

Part 3. Test Data

3.1 Unicorn Puzzle

Unicorn = [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T']]

UnicornSoST = [['-T']]

UnicornSoSH = [['-H']]

UnicornSoSnotU = [['U']]

UnicornSoSU = [['-U']]

Above is the unicorn puzzle we’ve been running with and the four possible conclusions we’re going to analyse to see if they follow from the puzzle knowledge base.

3.2 David-Putnam procedure example (prove S)

DP = [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R']]

DPSoS = [['-S']]

This is a problem discussed by Lila Kari in the Further Reading above to illustrate the David-Putnam procedure (which we don’t use here).

3.3 Kari’s example to illustrate the set of support procedure (prove P4)

Kari = [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6']]

KariSoS = [['-P4']]

This is Kari’s example to illustrate the set of support procedure we use here. It provides a longer and slightly more interesting proof.

3.4 The code to invoke the test runs.

print('\n', '====  Unicorn is Magical (prove T) ====')

PCRTP(Unicorn + UnicornSoST,UnicornSoST, 0)

print('\n', '====  Unicorn is Horned (prove H) ====')

PCRTP(Unicorn + UnicornSoSH,UnicornSoSH, 0)

print('\n', '====  Unicorn is not mythical (prove -U) ====')

PCRTP(Unicorn + UnicornSoSnotU,UnicornSoSnotU, 0)

print('\n', '====  Unicorn is Mythical (prove U) ====')

PCRTP(Unicorn + UnicornSoSU,UnicornSoSU, 0)

print('\n', '====  DP example (prove S) ====')

PCRTP(DP + DPSoS,DPSoS, 0)

print('\n', '====  Kari’s SoS example (prove P4) ====')

PCRTP(Kari + KariSoS,KariSoS, 0)

print('\n', '====  End of Examples ====')

Part 4: Running the Theorem Prover (test runs copied from Eclipse)

Review each run below with the top-level code of PCRTP at your side to see exactly how the theorem-prover executes. After a short while all will be completely clear!

4.1. Unicorn is Magical (prove T)

PCRTP(Unicorn + UnicornSoST, UnicornSoST, 0)

Iteration 0

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T']]

Current SoS =  [['-T']]

Current SoS clause =  ['-T']

New Resolvants =  [['-H']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H']]

New SoS =  [['-H']]

---

Iteration 1

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H']]

Current SoS =  [['-H']]

Current SoS clause =  ['-H']

New Resolvants =  [['-I'], ['-M']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H'], ['-I'], ['-M']]

New SoS =  [['-I'], ['-M']]

---

Iteration 2

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H'], ['-I'], ['-M']]

Current SoS =  [['-I'], ['-M']]

Current SoS clause =  ['-I']

New Resolvants =  [['-U']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H'], ['-I'], ['-M'], ['-U']]

New SoS =  [['-M'], ['-U']]

---

Iteration 3

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H'], ['-I'], ['-M'], ['-U']]

Current SoS =  [['-M'], ['-U']]

Current SoS clause =  ['-M']

New Resolvants =  [['U']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H'], ['-I'], ['-M'], ['-U'], ['U']]

New SoS =  [['-U'], ['U']]

---

Iteration 4

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-T'], ['-H'], ['-I'], ['-M'], ['-U'], ['U']]

Current SoS =  [['-U'], ['U']]

Current SoS clause =  ['-U']

New Resolvants =  [['M'], []]

empty clause found - proved

4.2. Unicorn is Horned (prove H)

PCRTP(Unicorn + UnicornSoSH,UnicornSoSH, 0)

Iteration 0

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-H']]

Current SoS =  [['-H']]

Current SoS clause =  ['-H']

New Resolvants =  [['-I'], ['-M']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-H'], ['-I'], ['-M']]

New SoS =  [['-I'], ['-M']]

---

Iteration 1

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-H'], ['-I'], ['-M']]

Current SoS =  [['-I'], ['-M']]

Current SoS clause =  ['-I']

New Resolvants =  [['-U']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-H'], ['-I'], ['-M'], ['-U']]

New SoS =  [['-M'], ['-U']]

---

Iteration 2

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-H'], ['-I'], ['-M'], ['-U']]

Current SoS =  [['-M'], ['-U']]

Current SoS clause =  ['-M']

New Resolvants =  [['U']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-H'], ['-I'], ['-M'], ['-U'], ['U']]

New SoS =  [['-U'], ['U']]

---

Iteration 3

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-H'], ['-I'], ['-M'], ['-U'], ['U']]

Current SoS =  [['-U'], ['U']]

Current SoS clause =  ['-U']

New Resolvants =  [['M'], []]

empty clause found - proved

4.3.  Unicorn is not mythical (prove -U)

PCRTP(Unicorn + UnicornSoSnotU,UnicornSoSnotU, 0)

Iteration 0

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U']]

Current SoS =  [['U']]

Current SoS clause =  ['U']

New Resolvants =  [['I']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I']]

New SoS =  [['I']]

---

Iteration 1

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I']]

Current SoS =  [['I']]

Current SoS clause =  ['I']

New Resolvants =  [['H']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I'], ['H']]

New SoS =  [['H']]

---

Iteration 2

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I'], ['H']]

Current SoS =  [['H']]

Current SoS clause =  ['H']

New Resolvants =  [['T']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I'], ['H'], ['T']]

New SoS =  [['T']]

---

Iteration 3

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I'], ['H'], ['T']]

Current SoS =  [['T']]

Current SoS clause =  ['T']

New Resolvants =  []

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I'], ['H'], ['T']]

New SoS =  []

---

Iteration 4

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['U'], ['I'], ['H'], ['T']]

Current SoS =  []

SoS empty  - cannot be proved

4.4.   Unicorn is Mythical (prove U)

PCRTP(Unicorn + UnicornSoSU,UnicornSoSU, 0)

Iteration 0

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U']]

Current SoS =  [['-U']]

Current SoS clause =  ['-U']

New Resolvants =  [['M']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M']]

New SoS =  [['M']]

---

Iteration 1

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M']]

Current SoS =  [['M']]

Current SoS clause =  ['M']

New Resolvants =  [['H']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M'], ['H']]

New SoS =  [['H']]

---

Iteration 2

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M'], ['H']]

Current SoS =  [['H']]

Current SoS clause =  ['H']

New Resolvants =  [['T']]

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M'], ['H'], ['T']]

New SoS =  [['T']]

---

Iteration 3

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M'], ['H'], ['T']]

Current SoS =  [['T']]

Current SoS clause =  ['T']

New Resolvants =  []

New Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M'], ['H'], ['T']]

New SoS =  []

---

Iteration 4

Current Base =  [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T'], ['-U'], ['M'], ['H'], ['T']]

Current SoS =  []

SoS empty  - cannot be proved

4.5. DP example (prove S)

PCRTP(DP + DPSoS,DPSoS, 0)

Iteration 0

Current Base =  [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R'], ['-S']]

Current SoS =  [['-S']]

Current SoS clause =  ['-S']

New Resolvants =  [['-Q', '-R'], ['P']]

New Base =  [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R'], ['-S'], ['-Q', '-R'], ['P']]

New SoS =  [['P'], ['-Q', '-R']]

---

Iteration 1

Current Base =  [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R'], ['-S'], ['-Q', '-R'], ['P']]

Current SoS =  [['P'], ['-Q', '-R']]

Current SoS clause =  ['P']

New Resolvants =  [['Q']]

New Base =  [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R'], ['-S'], ['-Q', '-R'], ['P'], ['Q']]

New SoS =  [['Q'], ['-Q', '-R']]

---

Iteration 2

Current Base =  [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R'], ['-S'], ['-Q', '-R'], ['P'], ['Q']]

Current SoS =  [['Q'], ['-Q', '-R']]

Current SoS clause =  ['Q']

New Resolvants =  [['-R', 'S'], ['-R']]

New Base =  [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R'], ['-S'], ['-Q', '-R'], ['P'], ['Q'], ['-R', 'S'], ['-R']]

New SoS =  [['-R'], ['-Q', '-R'], ['-R', 'S']]

---

Iteration 3

Current Base =  [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R'], ['-S'], ['-Q', '-R'], ['P'], ['Q'], ['-R', 'S'], ['-R']]

Current SoS =  [['-R'], ['-Q', '-R'], ['-R', 'S']]

Current SoS clause =  ['-R']

New Resolvants =  [[]]

empty clause found - proved

4.6. Kari’s SoS example (prove P4)           PCRTP(Kari + KariSoS,KariSoS, 0)

Iteration 0

Current Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4']]

Current SoS =  [['-P4']]

Current SoS clause =  ['-P4']

New Resolvants =  [['P1', 'P3']]

New Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3']]

New SoS =  [['P1', 'P3']]

---

Iteration 1

Current Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3']]

Current SoS =  [['P1', 'P3']]

Current SoS clause =  ['P1', 'P3']

New Resolvants =  [['P2', 'P3'], ['P5', 'P1']]

New Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1']]

New SoS =  [['P2', 'P3'], ['P5', 'P1']]

---

Iteration 2

Current Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1']]

Current SoS =  [['P2', 'P3'], ['P5', 'P1']]

Current SoS clause =  ['P2', 'P3']

New Resolvants =  [['P3'], ['P5', 'P2']]

New Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1'], ['P3'], ['P5', 'P2']]

New SoS =  [['P3'], ['P5', 'P1'], ['P5', 'P2']]

---

Iteration 3

Current Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1'], ['P3'], ['P5', 'P2']]

Current SoS =  [['P3'], ['P5', 'P1'], ['P5', 'P2']]

Current SoS clause =  ['P3']

New Resolvants =  [['P5']]

New Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1'], ['P3'], ['P5', 'P2'], ['P5']]

New SoS =  [['P5'], ['P5', 'P1'], ['P5', 'P2']]

---

Iteration 4

Current Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1'], ['P3'], ['P5', 'P2'], ['P5']]

Current SoS =  [['P5'], ['P5', 'P1'], ['P5', 'P2']]

Current SoS clause =  ['P5']

New Resolvants =  [['-P6']]

New Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1'], ['P3'], ['P5', 'P2'], ['P5'], ['-P6']]

New SoS =  [['-P6'], ['P5', 'P1'], ['P5', 'P2']]

---

Iteration 5

Current Base =  [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6'], ['-P4'], ['P1', 'P3'], ['P2', 'P3'], ['P5', 'P1'], ['P3'], ['P5', 'P2'], ['P5'], ['-P6']]

Current SoS =  [['-P6'], ['P5', 'P1'], ['P5', 'P2']]

Current SoS clause =  ['-P6']

New Resolvants =  [[]]

empty clause found – proved

END OF DOCUMENT