Saturday, July 27, 2013

Python 3 code for Resolution Theorem Prover

# 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 ====')