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

"The Quarry" by Iain Banks

From The Independent's review:

"The Quarry is set over a drunken, drug-addled weekend in a dilapidated old country house owned by Guy, a man in his early forties in the last stages of terminal cancer. The story is narrated by Kit, his 18-year-old son. Kit is on the spectrum of Asberger syndrome, and while that's a pretty familiar technique in modern literature Banks handles it brilliantly and injects something fresh into it – Kit's outlook on the world is not seen as a handicap necessarily, and is often an advantage, giving him a clearer view of the world than the jaded, confused and disappointed friends of Guy's who turn up for a weekend of reminiscing and airing of long-held grievances.

There are half a dozen former Film and Media Studies college mates of Guy's in attendance, all of them hitting 40, older but not necessarily wiser. Holly is a struggling movie critic, Paul is a corporate lawyer with an eye on a Tory candidacy, while Alison and Rob are a jargon-spouting couple who work for a search engine company. Completing the ensemble are Pris, a care worker, and Haze, a stoner with financial worries.

Banks has always been brilliant at ensemble writing, especially dialogue, and the vast majority of The Quarry is just that – drunken banter, acerbic asides, moments of touching honesty, political rants, and tirades of just about every other flavour.

There are three plot engines thrown into the mix but these are really red herrings, a familiar Banksian trope. Firstly, Kit is keen to find out the identity of his mother before Guy dies, as he has been raised by Guy in isolation his whole life. Secondly, there is the search for an apparently incriminating videotape that the gang made back in their youth. And thirdly, of course, there is the matter of Guy's imminent death, which hangs heavy over every action and conversation the group has.

The quarry of the title only comes into play latterly, a large gaping hole in the ground just past the garden wall of the house Guy lives in. Willoughtree House is to be knocked down when Guy dies and the rock beneath it dug out as part of the ever-expanding quarry, a metaphor for life and death that Banks plays with a delicate hand.

The true genius in The Quarry is twofold. Kit's deadpan narration is used not only to expose the petty squabblings of Guy and his entourage, but also to give a kind of clear-eyed pragmatism to life in the face of adversity. In contrast Guy is a gloriously awful creation, treating Kit like shit at every opportunity, ranting and raving about the state of the world, humanity, and his own shitty luck at dying too young.

Because ultimately, that's what The Quarry is all about.

It's a kind of raging against the dying of the light, but one mixed with an acute awareness of the nature of human frailties. Despite obvious outrage at every kind of social and personal injustice, and a deep sense of disappointment and failure that this generation hasn't done better, this is still, somehow, a profoundly humane, funny and smart novel, much like the author himself."

All the reviews have been pretty complimentary about Banks' last novel. Clare thought it was so-so - a meditation on our fading dreams as we age.

I beg to differ. Guy and his entourage are pretty stereotypical: the metropolitan Guardian left spouting 'Bliar'-type rants; really, none of it engages with deeper truth. These shallow creatures are not interesting and satirising them breaks no new ground. Guy's rants against the cancer which is killing him are well-written, colourful and frenetic but no-one with a brain could take his world-view seriously. Banks is surely too smart to be putting his personal impress on such superficiality, but this begs the question of why he even bothered creating the characters.

Really Mr Banks, you should have bowed out saying something more original; something more profound and interesting.

Speleologising ...

Into the underground at Burrington Coombe this afternoon with our leader, speleologist Chris. First off was Aveline's hole, where we got to see the  lines of crosses below, deep at the back of the cave. Chris is of the view that it's probably late palaeolithic, c. 14,000 years ago. As to why some bored hunter-gatherer sheltering from Arctic conditions post ice-age decided to scratch an upside-down version of Pascal's triangle using Xs is anyone's guess.

'Mesolithic' cave art in Aveline's Hole

Then on to Goatchurch Cavern where we slithered down way too many slippery steps into utter darkness. In the picture below Chris is pointing to some faint 'VV' inscriptions - warding symbols against the evil spirits which tend to blow out candles. The offending air-currents are caused by pressure changes as the water levels vary in air-filled cavities, often accompanied by shrieks and groans as the air is forced through small gaps in the rocks.

Clare and Chris ward off the witches deep underground

Goatchurch Cavern looking back to the entrance

Our leader's business card

I think we concluded that speleology is not for us.

"Love thy neighbour" .. why, exactly?

The following observation (Richard Dawkins, The Selfish Gene) has always struck me as both profound and politically illuminating.

"For relationships as distant as third cousin (2 x (1/2)⁸ = 1/128) we are getting down near the baseline probability that a particular gene possessed by A will be shared by any random individual taken from the population."

The 'population' we are talking about here is the co-ethnic population. For example, English people whose grandparents on both sides were also English.

What would you think if you saw someone walking down the street greeting everyone they met with a warm smile and a cheery greeting as if they were meeting their brother or sister? I'd cross over! People at less than 1% relatedness don't stir any innate kin-altruistic feelings in us. And so to the tragedy of the NHS and other 'caring' bureaucracies. Apart from rare super-empathic individuals (aka 'saints') most staff don't have any emotional investment in their clients at all - and why should they? So the default mode is neglect - as on the street. People who create social policies are often smart, highly urbane and empathic individuals who implicitly believe the masses are just like them. Organisations, processes and laws are repeatedly designed as if no-one would ever try to game them for their own convenience. If only!

The other implication concerns your personal contribution to the gene pool. After eight generations your descendants will be no closer genetically to you than a co-ethnic stranger today in the supermarket. So stop worrying about your spurious genetic immortality! But doesn't this contradict evolution? Not really: if the human race was today undergoing strong selection (i.e. lots of people were being killed off by the 'environment' before reproducing) then as a reproducing survivor your genes would disproportionally contribute, and skew, the future gene pool: they would matter. However, in advanced countries humanity today is subject only to weak selection - the gene pool is 'stationary' - so your contribution really doesn't matter at all.

Small caveat: if you're intelligent and civilised and don't reproduce, be aware that the rather dim and less civilised are reproducing just fine: they don't have the distractions of interesting career options. This of course also steers the gene pool so it's not quite stationary.

Presents *do* make a day

Of interest only to family members, Clare was recently 62 (nobody ever thinks they are going to be 62) and flatly stated a policy of no presents. This was widely disregarded as the following videos (downloadable) chronologically show.

1. Adrian's present.

2. My own offering.

3. Alex's present.

These are big files - hundreds of megabytes - and last between 3 and 5 minutes each so don't click unless you really want to see them.

"A Delicate Truth" - John Le Carre

In Gordon Brown's hapless fag-end government,  a young Ed Balls-like minister is in cahoots with an American right-wing private security company to illegally snatch a top jihadi from British Gibraltar.

Naturally,  this piece of incompetent free-enterprise goes horribly wrong leading to collateral damage (the death of innocents): also a blip in the career of said minister. The story doesn't die: an FO whistle blower is on the case and soon the cover-up is causing yet more collateral damage.

Don't you just hate those right-wing Republicans with their oodles of cash,  unlimited certainties and easy access to power?

Le Carre's novel is as beautifully written as always with a fine delineation of character. It's a shame, therefore, that the novel reads like a Guardian manifesto.

Wading through the unrelenting moralising at stereotyped hate-figures one eventually uncovers the flimsy plot. Yes, the operation went wrong .. but they often do. What happened is sad but completely unremarkable and would certainly not initiate the life-changing events Le Carre angrily recounts.

Like much of the novelist's recent work, 'A Delicate Truth' is merely an elegant rant.

Knightshayes Court and Heddon's Mouth

Can't keep us away from another neo-gothic pile, specifically Knightshayes Court near Tiverton with its beautifully manicured and vast woods and gardens. Note the 'woven horse' lurking behind Clare. In the afternoon we drove to the National Trust area of the Heddon Valley with its picturesque - albeit stony - walk to a rocky pebble beach.

A chilly sleeping bag, hard tent-base floor and 200 yard trek to the toilet block persuaded Clare to pack everything up this evening and return home: our mobile home in the Côte d'Azur recently has totally spoilt the girl. (I, however, need little persuasion to fall into line having an inordinate craving for luxury).

Here are the pix.

Knightshayes Court

There were woven deer too

Heddon's Mouth beach

The author fronting the river as it enters the sea

Camping on the river Exe

Our tent is pitched at the far end of a linear campsite,  abutting the river Exe which is about 12 foot wide  here running briskly over a rocky bed. It's making the sound that your WC makes when it won't stop flushing - some people would call that romantic but I'm wondering how well I'll sleep tonight.

These little midges flying around my head. I haven't been bitten (yet) but what do they live on?  What's the ecology? Cooing doves decorate the evening sky .. or pigeons infest the air with their raucous cries: you decide.

We visited Dunster Castle today in the heat and it was a delight,  the gardens populated with colourful, exotic plants. Our meal this evening in the pub local to the campsite was also rewarding - the landlord denied having wifi but seemed unaware I could piggyback on his BT Internet connection via BT FON. Bandwidth again after a day deprived!

Here are some pix. Dunster Castle,  a couple of pictures of us in our tent-home,  after our meal in the local pub. Apologies for such intense parochialism.

Dunster Castle

The old tent - up again

A babbling brook

The pub at Bridgetown

Gossip Cat: the elevator spiel

In "Accelerando", Charles Stross's novel, a central character is Aineko, the 'increasingly intelligent robot cat'. One day all cats will be like that but right now it's too hard. Gossip Cat is where we're at.

Gossip Cat is a phone app featuring a cat avatar you can chat with. It won't try to sell you anything and it won't just echo back what you just told it, Eliza-fashion.

GC will create a local knowledge-base of facts about your friends, neighbours and general gripes. It will incorporate built-in generic micro theories of personal behaviours and their consequences familiar from TV soaps. It will sympathise and pull its weight in conversation - in between soliciting food and personal grooming (it is a cat). The cat will be determinedly bland, banal and vacuous, reflecting its name and the state of the art in AI. How could it not go viral?
---
So here is my implementation plan.

0. Learn Python and the Eclipse SDK. I already learned that Python starts counting from zero :-). Thanks Alex for installing both.

1. Program a resolution theorem prover for propositional calculus. This sounds impressive but it's just a warm-up exercise - a hundred or so lines of code. This is a system which can solve tabloid recreational 'logic problems'.

2. Take a breather,  do the background research and program a resolution theorem prover for first order logic. This is quite hard and it will end up as the embedded inference engine for those micro theories.

3. Settle on the Gossip Cat functional architecture. This includes an extensible hierarchical ontology for the knowledge-base, a conversational model and text i/o parsing. I'd like to connect this to a third-party text-to-speech system. It'll be heavily top-down and model-based predictive as befits a conversational partner who isn't really paying you that much attention.

4. Now we get the CGI avatar to work - it's the user interface to the entire system. Hopefully there's some third-party library I can import,  otherwise I'll be on the  phone to my CGI-expert nephew Chris.

5. Time for kitty to pay a visit to the Android store and 'Hello World!'
---
Now, this has been a long elevator ride but if you're a venture capitalist and you stuck around, feel free to contact me with your cheque book open ;-).

Intermittent Fasting: month 11

Our holiday in France involved pleasant and sustained engagement with baguettes, confiture, camembert and rich gateaux. And way too much lounging around. The impact has been rather obvious. Still, in hand now.

Month	Date	Stone	Lb	Pounds	Kg	d(Lb)	BMI	Height (m)
0	07/08/2012	13	8	190	86.4		27.20	1.782
1	08/09/2012	12	13	181	82.3	9	25.91
2	06/10/2012	12	7	175	79.5	6	25.05
3	08/11/2012	11	12	166	75.5	9	23.76
4	08/12/2012	11	6	160	72.7	6	22.90
5	08/01/2013	11	2	156	70.9	4	22.33	Waist
6	10/02/2013	11	1	155	70.5	1	22.19	34.5 inches
7	09/03/2013	11	0.4	154	70.2	1	22.10
8	09/04/2013	10	12.2	152	69.2	2	21.79
9	11/05/2013	10	10.8	151	68.5	1	21.59	34 inches
10	11/06/2013	10	10.6	151	68.5	0	21.56
11	11/07/2013	10	13	153	69.5	-2	21.90

One slight change in the protocol. To optimise tissue-recovery and muscle-building after exercise, I have decided to eat on gym days. This means that once a week I get to spin the machines (as today) having fasted the previous day. Despite a cereal breakfast this morning, I was noticeably underpowered.