A Resolution Theorem Prover for the
Propositional Calculus
Nigel Seel, Interweave Consulting, Wells,
Somerset, UK. Version 1.0, July 27th
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:
- U -> I
- –U -> M
- I or M -> H
- 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:
- {-U, I}
- {U, M}
- {-I, H}
- {-M, H}
- {-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
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
