# This is the Python 3 code for a resolution theorem prover for the propositional calculus.
# Full documentation available from here.
'''
Created on 27 Jul 2013
@author: Nigel Seel
A Resolution Theorem Prover for Propositional Calculus
'''
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)
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
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)
''' --- Test Data ---
print(dedup([1, 2, 3, 4, 5]))
print(dedup([1, 2, 3, 2, 9, 3]))
print(dedup([]))
'''
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 = ['A', '-S', 'B', 'R']
then resolve(c1, c2) =
[['P', 'Q', 'S', 'A', '-S', 'B'], ['P', 'Q', '-R', 'A', 'B', '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
''' --- Test Data ---
c1 = ['P', 'Q', '-R', 'S']
c2 = ['-S', 'P', 'R']
print(resolve(c1,c2))
'''
#---------------------------------------------------
# The resolution procedure
def collectNewResolvants(Base, SoSclause):
newResolvants = []
for clause in Base:
newResolvants = newResolvants + resolve(clause,SoSclause)
return newResolvants
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)
# === Test Data ===
Unicorn = [['-U', 'I'], ['U', 'M'], ['-I', 'H'], ['-M', 'H'], ['-H', 'T']]
UnicornSoST = [['-T']]
UnicornSoSH = [['-H']]
UnicornSoSnotU = [['U']]
UnicornSoSU = [['-U']]
DP = [['-P', 'Q'], ['-Q', '-R', 'S'], ['P', 'S'], ['R']]
DPSoS = [['-S']]
Kari = [['-P1', 'P2'], ['-P2'], ['P1', 'P3', 'P4'], ['-P3', 'P5'], ['-P6', '-P5'], ['P6']]
KariSoS = [['-P4']]
# === 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 ====')
