Thoughts about 'Gossip'

'Gossip Cat ' is a project to build a cat avatar (running on a smartphone) which can gossip inconsequentially with the user.

My first thought was to model the content of gossip as a discussion about things. So Mrs Jones has a son,  we have established, and the cat asks "Did Mrs Jones' son visit recently? " This is toggling an attribute value in a record structure.

But really gossip is not like this. It's more like a soap opera: all about agents - their situation, problems, goals, intentions, beliefs and knowledge in as transgressive a context as possible.

This might lead in the direction of baroque epistemic-conative logics but that would be a category error. Instead we should define structural models of agent situations and 'states of mind' which lend themselves to algorithmic manipulation.

I'm thinking of front-ending this with a robust,  Eliza-like template-based natural language system.

A robust model of intentional dialogue,  even if highly content-bounded (there's a reason it's a cat!) could lead to an interesting theory: I think this is the order to do it.

Slugs

I was walking back from the gym this morning and had just entered a concrete path about 100 metres long which runs the length of a field to the right (figure 1), when I noticed two black slugs about a metre apart crossing the path with a trail of slime behind them.

'How likely is that?' I thought to myself. 'What are the chances of seeing any more?'

In fact there were no more. So what's going on here?

Figure 1 - markings in field are grass, not slugs!

Suppose the slugs are randomly distributed in the field . We imagine the path and field divided into a large number of cells as shown in figure 2 below, each of which may, or most likely not, contain a slug. (We only care about the row of cells along the path which we take to have the same distribution as the adjacent row in the field).

For each row, as we have a large number of cells (n large) and a small probability p of a slug being in any particular cell we can use the Poisson distribution. As we actually observed 2 slugs, our best estimate for the mean, μ = n * p, is 2.

The Poisson distribution calculator tells us that in this case the probability of seeing 3 or more slugs on the path (i.e. given μ = 2 what is  P(x>2 ?) is 32%.

That's way too high for me.

I prefer to reject the null hypothesis that the slugs were randomly distributed and take an alternative, that there was a slug family or cluster down there by the gate and they were crossing in a correlated way :-).

Figure 2

I was rubbish in the gym this morning, BTW. Like Chris Froome, reduced to eating a forbidden energy bar on the Tour de France, I ran out of energy pretty fast and also felt a twinge in my right knee. It was either the humidity (terrible today) or too much Alpen this morning just 90 minutes before I got started!
---
PS. Don't write me notes saying the chat about slugs above muddles the sample spaces - of course it does.

Try this: divide the path into two. In the first 50 metres we had n=50 and two slugs so the Poisson distribution applies as before with μ = 2. Assume the same distribution holds for the second 50 metres (the new sample space). The probability of seeing at least one slug there (according to the calculator)  is more than 86%.

But I didn't. So I think that sees off the random distribution hypothesis!

Badger Tales

Way past midnight I lie sleepless. Grunting and shuffling in the front garden below suggests much to an over-active imagination, but I know it's the badger, digging under our composting frame in search of egg shells. The next day brings confirmation: a new pit - plus strewn detritus.

We're rejoicing in our newly opened Waitrose (5 minutes walk away!) which we visited again two days after its opening on Thursday. We didn't need to dig a pit to get in: they were quite welcoming.

How happy were we?  Check the picture.

Wife and author: Waitrose fans

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