Friday, March 24, 2017

My ideal job: chief designer at Mind Design

Amazon link

Yesterday in a conversation with Clare the topic came up of my ideal job. No problem.

Since reading Greg Bear's Queen of Angels (years ago), I've wanted to be Roger Atkins.

But with a better name - obviously.

---

[AXIS (Automated eXplorer of Interstellar Space) is an AI system currently orbiting planet B-2 of Alpha Centauri B. Jill is the stay-at-home duplicate. -- From pp. 128-130.]

"LitVid 21/I A Net (David Shine): "We're preparing for an interview with Roger Atkins, chief designer at Mind Design Inc. responsible for AXIS's thinker device. What questions would you like to ask of the nation's foremost designer of thinking machines? For you know of course that thinking is different from computing.

"Roger Atkins regards computers as an architect might regard bricks. He is at this moment working with his massive personal construct thinking system, which he calls Jill, after an old, that is, a former girlfriend. Part of Jill is in fact the AXIS Simulation we have been mentioning throughout this vid-week, used to model the activities of AXIS itself, which is not directly accessible.

"But there are many more parts to Jill. Jill's central mind and most of her memory and analytical peripherals are on the grounds of Mind Design Inc near Del Mar, California; Jill can access other thinkers and analytical peripherals at Mind Design Inc facilities around the world, some by satellite, most by direct optical cable connections. While we speak with Mr. Atkins, we hope also to ask a few questions of Jill.

"And we begin right now. Mr. Atkins, in the past twenty five years you have moved from the status of a contracted neural network computer designer to perhaps the most important figure in artificial intelligence research. You seem to be in an ideal position to tell us why complete, self-aware artificial intelligence has proven to be such a difficult problem."

Atkins: "First of all, my apologies, but Jill is asleep right now. Jill has been working very hard recently and deserves a rest.

"Why is artificial intelligence so difficult? I think we always knew it would be difficult. When we say artificial intelligence, of course what we mean is something that can truly imitate the human brain. We've long since had thinking systems that could far outstrip any of us in basic computation, memorizing, and for the past few decades, even in basic investigative and creative thinking, but until the design of AXIS and Jill, they were not versatile. In one way or another, these systems could not behave like human beings.

"And one important consideration was that none of these systems was truly self-aware. We believe that in time Jill, and perhaps even AXIS itself, will be capable of self-awareness. Self-awareness is the most obvious indicator of whether we have in fact created full artificial intelligence."

David Shine: "There's a joke about self-awareness ... Could you tell it to us?"

Atkins: "It's not much of a joke. No human would laugh at it. But all modern workers in artificial intelligence have installed a routine that will, so to speak, 'laugh' or perceive humor in this joke should self-awareness occur in a system."

David Shine: "And what is the joke?"

Atkins: "It's embarrassingly bad. Someday perhaps I'll change it.

   'Why did the self-aware individual look at his image in the mirror?"

David Shine: "I don't know. Why did he?"

Atkins: "'To get to the other side.'"

David Shine: "Ha."

Atkins: "See, not very funny."

David Shine: "LitVid 21 viewer Elaine Crosby, first question to Mr. Atkins please."

LVV E Crosby Chicago Crystal Brick: "Mr. Atkins, I've read your lit, and I've long admired your work, but I've always been curious. If you do awaken Jill or some other machine, what will you tell them about our world? I mean, they'll be as innocent as children. How do you explain to them why society wants to punish itself, why we're so set on lifting ourselves up by our bootstraps whatever it takes, and we don't even know where we're going?"

Atkins: "Jill is hardly innocent. Just a few minutes ago, she was examining the theory of social feedback loops, that is, checks and balances in a society. She could probably tell us more about what troubles our society than any single human scholar.

"But that's just recreation for her, in a way; unless someone comes along and specifically asks us - or rather, rents Jill - she won't provide her analysis, but it'll be stored away. I doubt that even if she did solve our problems for us, we'd listen to her"

The novel was written in 1990, twenty seven years ago. Yet the narrative on AI is completely contemporary. The 'joke' is interesting: what humour it possesses would seem to reside in its character as a weak pun. Perhaps that just shows I'm not self-aware.

At time of writing, I suspect the leading candidate for Roger Atkin's job is Andrew Ng.

Thursday, March 23, 2017

Terror: can AI help?

My go-to guy on the Labour Left, Phil Burton-Cartledge, had this to say about yesterday's terror attack in central London.
"And, in a very rare instance, I'm going to defend the intelligence services. There is a very good chance the assailant was on a terror watch list. It's quite possible he had been or was presently under surveillance.

"Inevitably, the questions will be asked why he wasn't detected and/or picked up before now and prevented from undertaking this afternoon's attack. Again, while it's right such issues should be explored, lessons drawn and, if there is a case of egregious carelessness that those responsible be held to account, what really has to be asked is what could have been done differently?

Thankfully, we don't have indefinite detention without trial of suspects, but unless there are teams on standby covering the move of every single suspect then the answer has to be very little.

"Watching someone getting into their car and driving into central London is not immediately suggestive of suspicious activity. There is no way his intent to kill could be inferred before the car mounted the pavement and started accelerating towards passers by.

"This kind of attack is next to impossible to prevent if someone is so minded to carry it out."
These are very good points. But could AI have helped prevent the attack?

There are two issues to separate:
  • recognising that an attack is in progress
  • dealing with it.
Both are difficult.

Modern naval vessels are subject to attack from hypervelocity sea-skimming missiles. The time between detection and impact is short - too short to allow humans in the defence loop. The ship's AI monitors sensor systems such as radar, and has direct control over its terminal defence systems. An example would be the Phalanx.

If the AI gets it wrong and is too aggressive .. well, stuff happens in the military.

---

Deep Learning systems are typically trained on vast datasets, essential to extract the relevant classificatory features from the enormous space of relevant variations.
  • I doubt we have large datasets of events as rare and varied as 'Islamic terrorist attacks'.

  • I therefore doubt we could extract a definitive feature set which would reliably partition attacks from the myriad of events which define normal life.

Still, in more constrained situation such as an entranceway, you could create plenty of simulation data of intruders armed with knives or guns and I suspect a recogniser could be made to work. The police or guards would call in an attack anyway, so the AI system might buy you only a few seconds (and I'd be worried about all those false positives and false negatives).

But it would really come into its own if it could be linked to a fast response system.

I rather admire those security guys who take-down armed assailants. Almost all of the time on their watch, nothing bad is happening. Then comes an exceedingly rare event which they have to classify within seconds as requiring lethal force - and get it right. The natural human reaction would be to hold off for fear of making a catastrophic error. It's a hard call.

In Richard K. Morgan's SF pulp noir "Altered Carbon", the AI system at the 'Hendrix Hotel' takes out hero Takeshi Kovacs's attackers (once he has thumb-printed his contract!):
"I straightened again and snapped my hand out to the keypad beside the screen. Traces of fresh spittle smeared over the matt black receiver. A split second later a calloused palm edge cracked into the left side of my skull and I collapsed to my hands and knees on the floor. A boot lashed into my face and I went the rest of the way down.

'Thank you sir.' I heard the voice of the hotel through a roaring in my head. 'Your account is being processed.'

I tried to get up and got a second boot in the ribs for the trouble. Blood dripped from my nose onto the carpet. The barrel of the gun ground into my neck.

'That wasn't smart, Kovacs.' The voice was marginally less calm. 'If you think the cops are going to trace us where you're going, then the stack must have fucked your brain. Now get up! '

He was pulling me to my feet when the thunder cut loose.

Why someone had seen fit to equip the Hendrix's security systems with twenty-millimetre automatic cannon was beyond me, but they did the job with devastating totality. Out of the corner of one eye I glimpsed the twin-mounted auto-turret come snaking down from the ceiling just a moment before it channelled a three-second burst of fire through my primary assailant. Enough fire-power to bring down a small aircraft. The noise was deafening. "
Decisions which seem difficult when you're thinking at human speeds seem a lot more tractable when time is slowed by a factor of ten or one hundred .. or when thinking speed is cranked up by a similar amount.

Something tells me the Hendrix Hotel is the way of the future.

Wednesday, March 22, 2017

A star orbitally skimming a black hole

Centauri Dreams had a post yesterday describing the unusual system 47 Tuc X9 which is 14,800 light years from Earth. It appears to be a white dwarf star in a very close orbit (radius about a million kilometres) around a black hole, with orbital period 28 minutes (!).

The post is illustrated by an artist's impression of the system:



and a statement of the curious orbital dynamics:
"This white dwarf is so close to the black hole that material is being pulled away from the star and dumped onto a disk of matter around the black hole before falling in,” says lead author Arash Bahramian (University of Alberta and Michigan State University). “Luckily for this star, we don’t think it will follow this path into oblivion, but instead will stay in orbit. ...

"We think the star may have been losing gas to the black hole for tens of millions of years and by now has now lost the majority of its mass. Over time, we think that the star’s orbit will get wider and wider as even more mass is lost, eventually turning into an exotic object similar to the famous diamond planet discovered a few years ago."
It isn't obvious why the star is winding its way out from the black hole and several commentators get confused (hint: it's not frame-dragging).

From the star's period and orbital radius we can work out the mass of the black hole: 94 solar masses. From this, we can calculate the black hole's schwarzschild radius - an event horizon of 277 km, just under 100 times larger than the event horizon of a solar mass black hole (3 km).

The black hole's gravity at the orbital radius of the star is 13.4 km/sec2, or just under 1,400g. You can see why it's whipping around so fast (c. 3,300 km/sec or 1% of the speed of light).

Try to imagine it. If this black hole were placed at the centre of the Earth, it would be an unimaginably tiny object (277 km!) in the middle of the core. The star, meanwhile, is two and a half times the distance of the Moon. The star's experience of the black hole comes down to some pretty crazy tidal forces.

We know about tidal forces: they try to tear the star apart and rearrange its material into an orbital ring. None of this would explain material infalling into the black hole or the star spiralling outwards. We don't see such phenomena at Saturn for example.

The secret is explained by the authors in this remark:
"Low mass X-ray binaries (LMXBs) are systems in which a compact object [neutron star (NS) or black hole (BH)] accretes matter from a low mass companion (typically a main sequence star) through Roche-lobe overflow or wind-fed accretion (from a red giant). ...

"In the most likely scenario, this particular star would have first started losing mass to the suspected black hole several tens of millions of years ago when it was much closer, in an orbit with a period of just minutes.

"Over time, as that star has lost most of its mass, the size of the orbit would have increased, and the rate at which mass has been lost to the black hole would have decreased. The rate of mass loss would once have been a billion times higher. So yes, the star would initially have been much closer to the black hole.

"How close a star can get to a black hole before starting to lose mass to the black hole depends on the kind of star it is. Big, fluffy giant stars can lose gas to a black hole when they are much further away than small, compact stellar remnants like this white dwarf, whose gravity is strong enough that they are able to hold onto their mass more tightly, so need to get much closer before mass can be torn away.

"We also think that this star will have been gradually losing mass over tens to hundreds of millions of years; in this case it is not being torn apart in a single cataclysmic event that results in it being shredded into streams of debris, as we have seen in spectacular outbursts from the centres of some external galaxies (known as tidal disruption events).

"Rather, in this case, we have a steady loss of mass to the black hole over time."
The Roche-lobe overflow effect is an interesting one (Wikipedia article). If debris from the star can reach the L1 Lagrange point (between the star and the black hole) it can migrate to the black hole itself. The remaining stellar material has higher than before angular momentum and its orbital radius increases. [Note: but apparently not - see comments.]

Roche Lobe potential: from the Wikipedia article

There are few things more counter-intuitive than orbital mechanics.

How language irritates!

Yesterday the BBC News carried long minutes of programming devoted to the life of Martin McGuinness: warrior/terrorist turned statesman/peacemaker in the official narrative.

And there were repeated references to 'Londonderry'.

Yes, Derry is called 'Londonderry' whenever the BBC wants to line up behind the Unionists; it used to be a signifier for a nationalist atrocity. Conversely, whenever the Protestants did something awful to the Catholics, we'd hear about 'Derry'.

I was shouting at the TV: "It's Derry!".

---

There was a moment when the media got confused about the US/UK laptop/tablet hand-baggage ban on flights from the Middle-East. The BBC Newsreader put on her best pinched moue and spoke of the ban on flights from 'six mainly-muslim' countries.

This recent stock-phrase, 'mainly-muslim', is virtue-signalling for "You are a right-wing Islamophobe and we are better than you'.

Then they discovered that the bans were not Trump-fascism but a sensible and graduated intelligence-led assessment based on well-founded threats from ISIS ('so-called Islamic State'). Suddenly, 'mainly-muslim' was dropped and it became: 'flights from six Middle-Eastern countries'.

And I was able to stop shouting at the TV.

Tuesday, March 21, 2017

"International Trotskyism 1929–1985"

Robert J. Alexander wrote this magisterial tome in 1991: "International Trotskyism 1929–1985: A Documented Analysis of the Movement".




At 1,141 pages and out of print, it is a labour which will surely never be repeated. However, the PDF exists on the Internet and you can download it here.

The history of the International Marxist Group, the IMG is covered in pages 492-496. The quote from my previous post, on the occasion of Martin McGuinness's death, is on page 493.

There is a detailed and somewhat critical review of the book here (1993).

"Victory for the IRA"

In 1972 I was a member of the International Marxist Group as we marched through London in support of the Irish struggle.

Martin McGuinness: 23 May 1950 – 21 March 2017

The IMG became rather notorious for its slogan: "Victory for the IRA"*. I was present at the leadership committee where this was discussed. Tariq Ali was the main proponent, arguing in his typical romantic-revolutionary way that the IRA were so vilified by the British establishment that we revolutionaries - in the belly of the beast - were morally obligated to stand against the current and show our full solidarity for the national liberation struggle.

John Ross, who I supported, argued mildly that we thoroughly disapproved of the IRA's campaign of voluntarist violence and bombings. Nevertheless we were duty bound to be in solidarity with their anti-imperialist struggle, and that the correct, Marxist slogan was "Solidarity with the IRA".

He was undoubtedly correct, but Tariq's élan won the day.

I remember marching on the streets, braving the hostility of the watching crowds and the contempt of the stewarding police, chanting "Victory .. to .... the IRA!" and feeling proud of my party discipline even as I compounded its error. It was not clear to any of us what a 'victory' for the IRA would even look like.

Interestingly​, on the occasion of  Martin McGuinness's death, we've not moved on that much.

---

* The quote is from this book.

Improved resolution theorem prover (RTP v. 1.1)

You will have previously seen the announcement about the first (tutorial) version of my resolution theorem prover in Lisp.

Today I'm releasing version 1.1 which is easier to use and gives a clearer output.

Below are the "Who does Lady Sally Fowler like?" proofs (compare with the previous version).

The code is available at the AI code in Lisp Resource on the right of your (web view) screen.

Or follow these links for the program file and genealogical test data.

Retrieve program file: RTP-v1.1 and test-data:  Genealogical-etc-test-data.


---    To determine (likes sally ?who)    ---

 > (prove-it *g-mge1* *mge-axioms* 8)

Do you want to see all the proof steps y/n?  n
Conclusion = ((<- ((LIKES SALLY SALLY))))

(13)   ((LIKES ?X ?X) <-)
(14)   (<- ((LIKES SALLY ?WHO)))
(19 14 13)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY ROD))))

(5)   ((LIKES SALLY ROD) <-)
(14)   (<- ((LIKES SALLY ?WHO)))
(16 14 5)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY RENNER))))

(4)   ((LIKES SALLY RENNER) <-)
(14)   (<- ((LIKES SALLY ?WHO)))
(15 14 4)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY MOTIES))))

(13)   ((LIKES ?X ?X) <-)
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(14)   (<- ((LIKES SALLY ?WHO)))
(17 14 10)   (<- ((LIKES ?WHO MOTIES)))
(24 17 13)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY HORVATH))))

(9)   ((LIKES HORVATH MOTIES) <-)
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(14)   (<- ((LIKES SALLY ?WHO)))
(17 14 10)   (<- ((LIKES ?WHO MOTIES)))
(20 17 9)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY SALLY))))

(13)   ((LIKES ?X ?X) <-)
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(14)   (<- ((LIKES SALLY ?WHO)))
(17 14 10)   (<- ((LIKES ?WHO MOTIES)))
(21 17 10)   (<- ((LIKES MOTIES MOTIES)))
(27 21 13)   +EMPTY-CLAUSE+
-----------------------------------
---

RTP Release 1.1 description.

Version 1.1: 21st March 2017

Use with test data file:  Genealogical-etc-test-data   ('load' statement at end of the file).

Version 1.01 continues to be best as a first tutorial to understand the program at code level. Plenty of comments there showing worked-execution. But the process for the user to invoke the program is clumsy.

This version has:
  1. Stripped out many of the comments for improved code clarity.
  2. Wrapped up execution in a new function, 'prove-it'.
  3. Improved functions to print the proofs created by the program. 
All new functions at the end of the file.

Only other change is altered search strategy order in 'prove1':

.       (next-igb-list     (append new-igb-list igb-list1)) ) ; search strategy

which seems to help convergence.

---

The main test data for the new version is the genealogical axiom set which you will find in the test data mentioned above (or for an early version scroll to the bottom here).

It does lead to some tortuous proofs: for example, this one.

---

> (defvar *gg6* (mk-goal-clause '((grandfather gerry james))))

> (prove-it *gg6* *family-tree-axioms* 12)
Conclusion = ((<- ((GRANDFATHER GERRY JAMES))))

(13)   ((CHILD-OF PETER JANE JAMES) <-)
(2)   ((MALE PETER) <-)
(11)   ((CHILD-OF GERRY MARY PETER) <-)
(1)   ((MALE GERRY) <-)
(23)   ((PARENT ?X ?Z) <- ((MALE ?X) (CHILD-OF ?X ? ?Z)))
(23)   ((PARENT ?X ?Z) <- ((MALE ?X) (CHILD-OF ?X ? ?Z)))
(1)   ((MALE GERRY) <-)
(32)   ((GRANDFATHER ?X ?Z) <- ((MALE ?X) (PARENT ?X ?Y) (PARENT ?Y ?Z)))
(39)   (<- ((GRANDFATHER GERRY JAMES)))
(40 39 32)   (<- ((MALE GERRY) (PARENT GERRY ?Y1425) (PARENT ?Y1425 JAMES)))
(41 40 1)   (<- ((PARENT GERRY ?Y1425) (PARENT ?Y1425 JAMES)))
(42 41 23)   (<- ((PARENT ?Y1425 JAMES) (MALE GERRY) (CHILD-OF GERRY ?1498 ?Y1425)))
(44 42 23)   (<- ((MALE GERRY) (CHILD-OF GERRY ?1498 ?Y1425) (MALE ?Y1425) (CHILD-OF ?Y1425 ?1547 JAMES)))
(46 44 1)   (<- ((CHILD-OF GERRY ?1498 ?Y1425) (MALE ?Y1425) (CHILD-OF ?Y1425 ?1547 JAMES)))
(47 46 11)   (<- ((MALE PETER) (CHILD-OF PETER ?1547 JAMES)))
(49 47 2)   (<- ((CHILD-OF PETER ?1547 JAMES)))
(50 49 13)   +EMPTY-CLAUSE+
-------------------------------------- 

So that means it's already a superhuman reasoner, right?

Monday, March 20, 2017

AI code in Lisp: new resource here

New resource on the sidebar to your right. This should please readers wondering why vast screeds of Lisp code randomly appear here, interrupting more erudite essays on this & that.

Except as I write this, 134 of you have visited: Description: Theorem Prover in Lisp.

Here's what the READ ME at the new sidebar says.

READ ME
=======

These Common Lisp files contain AI programs which are organised around the theme of building a chatbot.

They will all run independently and were developed in LispWorks free Personal Edition.

You can use the code as you like. It's not supported and there will certainly be bugs I haven't spotted.

I think of the code as a toolkit, there to be modified.

---

To come:

1. Upgrades to the resolution theorem-prover improving the display of proofs + any bug fixes.

2. An AI planner, oriented both towards a toy, virtual, physical world and speech acts for conversation planning.

3. A design for 'internal emotional states' to create some 'point' for the chatbot's autonomous behaviour; we need something more interesting than a natural language interface to Wikipedia-style queries.

Plus integration of all the above.

Sunday, March 19, 2017

Readings to Clare

I assume some people liked my audio recording of "The Mote in God's Eye"?

There's a new tab on the right: 'Readings to Clare'.

Here's the directory:



The books marked +....-abandoned I didn't finish. They didn't work for one reason or another as books to be read aloud to Clare. You get the earliest chapters, but then .. abandoned.

  • Game of Thrones is good. I abandoned the sequel, as the action began to slow down in the middle of the second volume. We saw the TV series instead.

  • The Patrick Lee books are uniformly excellent, but unfortunately I did not record the first book, 'The Breach', in the 'Breach' sequence. You'll have to get that for yourself.

  • There is one early chapter omitted in 'Conclave' (accident of uploading) but I summarise each chapter at the start of the next reading so it's not a show-stopper. Conclave is, in any case, excellent.

  • I was not especially impressed by Lee Child's book, nor Philip Kerr's.

  • Ursula Le Guin's Earthsea books are excellent and I will be reading the rest of the sequence in time.

  • I am currently reading 'Darkness at Noon' - that's in progress.

Here's Clare, about to go out yesterday.



Thursday, March 16, 2017

Description: Theorem Prover in Lisp

[Update: RTP release 1.1 is now available.]
---

As I mentioned, I've now completed basic testing of my (very, very simple) resolution theorem prover in Common Lisp: the code is ready to load. But read the stuff below first.

1. How to run the system

Once you have the code in front of you, go to Part 2: clauses and extended clauses where you will find the test-data definitions as follows:
(defvar *c1* (mk-fact-clause '(member ?item (?item . ?rest ))))
(defvar *c2* (mk-rule-clause '(member ?item (? . ?rest)) '((member ?item ?rest))))
(defvar *c3* (mk-fact-clause '(likes rod horvath)))
(defvar *c4* (mk-fact-clause '(likes sally renner)))
(defvar *c5* (mk-fact-clause '(likes sally rod)))
(defvar *c6* (mk-fact-clause '(likes hardy renner)))
(defvar *c7* (mk-fact-clause '(likes hardy rod)))
(defvar *c8* (mk-fact-clause '(amusing hardy)))
(defvar *c9* (mk-fact-clause '(likes horvath moties)))
(defvar *c10* (mk-rule-clause '(likes sally ?x) '((likes ?x moties)) ) )
(defvar *c11* (mk-rule-clause '(likes rod ?x) '((likes ?x renner) (likes ?x rod))))
(defvar *c12* (mk-rule-clause '(likes ?x ?y) '((amusing ?y) (likes rod ?y)) ) )
(defvar *c13* (mk-fact-clause '(likes ?x ?x)))

(defvar *g1* (mk-goal-clause '((likes sally ?who))))
(defvar *g2* (mk-goal-clause '((member sally (rod renner horvath sally . moties)))))

(setf *axioms* (list *c1* *c2* *c3* *c4* *c5* *c6* *c7* *c8*
                 *c9* *c10* *c11* *c12* *c13*))

(setf *goals* (list *g1*))
Input your own facts, rules and goals and assign them to variables *axioms* and *goals* as shown above. Or just use my test data to check the system out in the first instance.

Now go to Part 4:  TEST DATA and execute the following commands as shown there.
(defvar *igb-list-ia-list* (initialise-databases *goals* *axioms*))

(defvar *igb-list* (first *igb-list-ia-list*))  ; extended goal clause(s)

(defvar *ia-list*   (second *igb-list-ia-list*))  ; extended axiom clauses

(setf archived-goals-and-proofs (prove *goals* *axioms* 6))    ; depth 6 here

(pprint (setf all-proofs (show-all-proofs archived-goals-and-proofs *ia-list*)))
The search depth (eg 6) is arbitrary - try 4 or 8 etc.

With *1step* set to true,
(defvar *1step* t)        ; If t stops proof loop each iteration and
;                                      prints archived-goals, archived proofs & next goals
the theorem-prover will print its workings on each inference cycle and wait for input before proceeding. If you just want the thing to run to completion, set *1step* to nil.

---

2. In-code documentation

Most of the code is heavily documented with runtime examples - but read this post first.

---

3. Data Structures

The data structures are as follows.

1. We start with literals like (LIKES ?X RENNER), (LIKES SALLY ?WHO) - which the function 'unify' tries to unify to create bindings like this:
((?WHO . RENNER) (#:?X1113 . SALLY)).

2. At the level of basic binary resolution we have clauses, which look like this:

A fact is a clause (a list of literals) which contains only one (positive) literal followed by <- .
(defvar *c1* '( (likes horvath moties) <- )                          ; a fact clause
A rule is a clause (a list) which is a (positive) literal (the clause head) followed by <- and then a list of literals - the body of the clause.

We use <- with value nil as a spacer only for human readability.
(defvar *c2* '((likes sally ?who) <- ((likes ?who ?y) (likes ?y moties)))     ;  rule
A goal is a clause (a list) of one or more negative literals. First element is <- for human readability.
(defvar *g* '(<- ((likes ?x renner) (likes ?x rod)) ) )          ;  a goal clause

3. At the level of running the whole proof procedure we have extended-clauses, sometimes written as igb-list and ia-list for extended goal clauses and extended axiom clauses. The letter 'i' stands for index, and 'b' stands for binding.

An extended clause is a triple: index,  clause, then (if a goal) binding. It is implemented as a list like this: (index clause binding). Example:
(defvar *icb* '((16 (4 (nil nil)) (2 (nil nil)))                   ; Index
                     (<- ((likes ?x renner) (amusing ?x)))       ; Clause
                              ((T . T))))                                    ; Binding
An index is a binary tree of integers, with leaves nil.
Example: (1 (nil nil))   or   (16 (12 (7 (nil nil)) (4 (nil nil)) ) (5 (nil nil)) )
Each leading integer is the current clause number; the two immediate children are the two resolution parent clauses .. and so on. Initial goals, and axioms have no parents, thus nil.

The reason for extended clauses is that we need to keep track of the inference steps to reconstruct the entire proofs afterwards. The bindings are kept to allow us to instantiate variables in the original query which we need as the answer!

---

4. FAQs (reprinted from here).

4.1. Isn't this just Prolog?

Prolog is encountered as a black box. You provide a program and a query (as above) and you get back bindings, like this:
?- likes(sally, W).

W = sally;
W = rod;
... and so on

If you want proofs, to add the 'occurs check' or to change the order in which resolution steps are tried (the search strategy) - well tough: all those things are both fixed and opaque in Prolog. To make them explicit for modification, you have to write an explicit theorem-prover in Prolog (which can of course be done).

4.2. You are using Horn clauses?

Yes. I initially thought to implement a general clausal prover, but Horn clauses make the resolution step particularly simple (just one positive literal to match) and you lose neither generality nor expressive power. But since everything in the code is both modular and explicit, it would be easy to extend the program.

4.3. The style is functional?

Yes. Resolution theorem provers on the Internet are heavily optimised with clever, imperative algorithms and direct access data structures such as hash tables. This makes the code efficient but obscure - very hard to understand.

I didn't want to do that. This is a tool-kit and I'm not trying to create thousands of logical inferences per second. My intended application area (simple inference over an ever-changing knowledge-base for a chatbot) never requires massive inferential chains so clarity and easy modifiability was my objective.

4.4. What was hard?

The program is architected at three levels.

(a) Unification

This is basically already quite modular and straightforward. I re-used Peter Norvig's code.

(b) Resolution

Binary resolution itself - specially with Horn clauses - is a straightforward procedure - as you will see in the code. There are some subtleties with bindings and substitutions, but once you realise that resolution is fundamentally a local operation it's not too difficult.

(c) Control and proof construction

The process of creating new goals and resolving them with the axioms is somewhat complex although again, sticking with Horn clauses makes it a lot easier: just think of a naive Prolog execution model.

However, if you want to return proofs, you need to number the axioms and number-and-archive goals as you process them, capturing the resulting tree of inferences. At the end, for each empty-clause = successful proof, you need to trace that index-tree backwards to recover the proof steps. I found it a bit intricate.

4.5. What's next?

In theory you can do anything with a theorem-prover (Prolog being the existence proof) but it's not necessarily the best architecture. For a planner, where state changes are part of the problem definition, I need to adapt the tool-kit to a design centred around actions with pre- and post-condition in the context of a goal-state and an updating world-state. Such a dynamic model can be used both for actions in a (virtual) world and conversation planning via speech acts.

The theorem-prover remains optimal as a separate module, managing the crystallized knowledge base using inference to draw conclusions - for example to drive questions and answers.

I'm thinking of using the already-programmed Eliza front-end as a robust conversational interface. Doesn't matter if it's bluffing some of the time if it can use learning, inference and planning often enough.

Onwards to the GOFAI smart chatbot ...

---

5. Miscellaneous

As usual, code is provided for free use, unsupported and with no guarantees at all that there aren't bugs I've missed. Feel free to tell me in the comments.

Other code you may find useful:
  1. A resolution theorem prover in Lisp (as described here)
  2. Prolog in Lisp
  3. Minimax (noughts-and-crosses) in Lisp
  4. Eliza in Lisp
 An example of input and output of the prover.

---

Update: Saturday March 18th 2017.

1. Code here slightly updated (to v. 1.01) with change to 'show-proof' (and 'show-all-proofs') to add an additional 'top level goals' parameter, thereby getting rid of the previous embedded global variable. This makes the code completely functional now.

2. With further testing (on the genealogical axiom set below) .. with deeper inferences .. I have noticed that naive pprint doesn't do a good job of showing the output - the 'found proofs'. Over the next few days I'll write a dedicated display function which can handle more deeply-nested proofs and let you know when it's done. I'll also provide you with proper version of the genealogical test data below: (not completed testing, so it's illustrative only at this point).

; ---  Test data: family tree : axioms and goal ---
;   https://jameskulkarni17.wordpress.com/2011/09/26/family-tree-using-prolog/
;   with anglicised names and modified rules.

(defvar *g1* (mk-fact-clause '(male gerry)))
(defvar *g2* (mk-fact-clause '(male peter)))
(defvar *g3* (mk-fact-clause '(male john)))
(defvar *g4* (mk-fact-clause '(male mike)))
(defvar *g5* (mk-fact-clause '(male james)))
(defvar *g6* (mk-fact-clause '(male hugo)))

(defvar *g7* (mk-fact-clause '(female mary)))
(defvar *g8* (mk-fact-clause '(female jane)))
(defvar *g9* (mk-fact-clause '(female sarah)))
(defvar *g10* (mk-fact-clause '(female christine)))


(defvar *g11* (mk-fact-clause '(child-of gerry mary peter)))
(defvar *g12* (mk-fact-clause '(child-of gerry mary john)))
(defvar *g13* (mk-fact-clause '(child-of peter jane james)))
(defvar *g14* (mk-fact-clause '(child-of peter jane mike)))
(defvar *g15* (mk-fact-clause '(child-of john sarah christine)))
(defvar *g16* (mk-fact-clause '(child-of john sarah hugo)))


(defvar *g17* (mk-fact-clause '(brother peter john)))
(defvar *g18* (mk-fact-clause '(brother john peter)))
(defvar *g19* (mk-fact-clause '(brother james mike)))
(defvar *g20* (mk-fact-clause '(brother mike james)))

(defvar *g21* (mk-fact-clause '(brother hugo christine)))
(defvar *g22* (mk-fact-clause '(sister christine hugo)))

(defvar *g23* (mk-rule-clause '(parent ?X ?Y) '((child-of ?X ? ?Y))))
(defvar *g24* (mk-rule-clause '(parent ?X ?Y) '((child-of ? ?X ?Y))))

(defvar *g25* (mk-rule-clause '(sibling ?X ?Y) '((brother ?X ?Y))))
(defvar *g26* (mk-rule-clause '(sibling ?X ?Y) '((sister ?X ?Y))))

(defvar *g27* (mk-rule-clause '(father ?X ?Z) '((child-of ?X ? ?Z))))

(defvar *g28* (mk-rule-clause '(mother ?Y ?Z) '((child-of ? ?Y ?Z))))

(defvar *g29* (mk-rule-clause '(son ?X ?Y ?Z)
                              '((male ?X) (father ?Y ?X) (mother ?Z ?X))))

(defvar *g30* (mk-rule-clause '(daughter ?X ?Y ?Z)
                              '((female ?X) (father ?Y ?X) (mother ?Z ?X))))

(defvar *g31* (mk-rule-clause '(wife ?X ?Y) '((female ?X) (child-of ?Y ?X ?))))

(defvar *g32* (mk-rule-clause '(grandfather ?X ?Z)
                              '((male ?X) (parent ?X ?Y) (parent ?Y ?Z))))

(defvar *g33* (mk-rule-clause '(grandmother?X ?Z)
                              '((female ?X) (parent ?X ?Y) (parent ?Y ?Z))))

(defvar *g34* (mk-rule-clause '(uncle ?X ?Z)
                              '((male ?X)   (sibling ?X ?Y) (parent ?Y ?Z))))

(defvar *g35* (mk-rule-clause '(aunt ?X ?Z)
                              '((female ?X) (sibling ?X ?Y) (parent ?Y ?Z))))

(defvar *g36* (mk-rule-clause '(cousin ?X ?Y)
                              '((parent ?U ?X) (sibling ?U ?W) (parent ?W ?Y))))

(defvar *g37* (mk-rule-clause '(ancestor ?X ?Y ?Z) '((child-of ?X ?Y ?Z))))
(defvar *g38* (mk-rule-clause '(ancestor ?X ?Y ?Z)
                              '((child-of ?X ?Y ?W)  (ancestor ?W ? ?Z))))

(defvar *family-tree-axioms* (list *g1* *g2* *g3* *g4* *g5* *g6* *g7*
                                 *g8* *g9* *g10* *g11* *g12* *g13*
                                 *g14* *g15* *g16* *g17* *g18* *g19*
                                 *g20* *g21* *g22* *g23* *g24* *g25*
                                 *g26* *g27* *g28* *g29* *g30* *g31*
                                 *g32* *g33* *g34* *g35* *g36* *g37* *g38*))

(defvar *gg1* (mk-goal-clause '((father ?X ?Y))))
(defvar *gg2* (mk-goal-clause '((mother ?X ?Y))))
(defvar *gg3* (mk-goal-clause '((child-of ?X ?Y ?Z))))
(defvar *gg4* (mk-goal-clause '((son james ?X ?Y))))
(defvar *gg5* (mk-goal-clause '((daughter christine ?X ?Y))))
(defvar *gg6* (mk-goal-clause '((grandfather ?X ?Y))))
(defvar *gg7* (mk-goal-clause '((aunt ?X ?Y))))
(defvar *gg8* (mk-goal-clause '((uncle peter ?X))))
(defvar *gg9* (mk-goal-clause '((cousin ?X ?Y))))
(defvar *gg10* (mk-goal-clause '((ancestor ?X ?Y james))))

(defvar *family-tree-goal* (list *gg1* ))   ; start testing with the first goal

;;; A function, 'prove-it', to save copy-and-paste of the long commands below

(defun prove-it (goal depth)
    (setf *igb-list-ia-list*
        (initialise-databases *family-tree-goal* *family-tree-axioms*))
    (setf *igb-list* (first *igb-list-ia-list*))
    (setf  *ia-list*  (second *igb-list-ia-list*))
     (setf archived-goals-and-proofs (prove (list goal) *family-tree-axioms*  depth))
     (pprint (setf all-proofs
                           (show-all-proofs archived-goals-and-proofs *ia-list* (list goal))))
 nil)

#|   --- Commands to run the test data ---

(defvar *igb-list-ia-list*
        (initialise-databases *family-tree-goal* *family-tree-axioms*))
(defvar *igb-list* (first *igb-list-ia-list*))
(defvar *ia-list*  (second *igb-list-ia-list*))

(setf archived-goals-and-proofs (prove *family-tree-goal* *family-tree-axioms*  6))

(pprint (setf all-proofs (show-all-proofs archived-goals-and-proofs *ia-list* *family-tree-

goal*)))

or type

(prove-it *gg1* 6)    ; but currently doesn't display well

----------------------------------------------------------------------------------
|#

#|
**********************   Intended Output   *************************

(defvar *gg1* (mk-goal-clause '((father ?X ?Y))))

1 ?- father(X,Y).

X = gerry
Y = peter ;

X = gerry
Y = john ;

X = peter
Y = james ;

X = peter
Y = mike ;

X = john
Y = christine ;

X = john
Y = hugo ;

No
******************************************************
(defvar *gg2* (mk-goal-clause '((mother ?X ?Y))))

2 ?- mother(X,Y).

X = mary
Y = peter ;

X = mary
Y = john ;

X = jane
Y = james ;

X = jane
Y = mike ;

X = sarah
Y = christine ;

X = sarah
Y = hugh ;

No
******************************************************
(defvar *gg3* (mk-goal-clause '((child-of ?X ?Y ?Z))))

3 ?- child-of(X,Y,Z).

X = gerry
Y = mary
Z = peter ;

X = gerry
Y = mary
Z = john ;

X = peter
Y = jane
Z = james ;

X = peter
Y = jane
Z = mike ;

X = john
Y = sarah
Z = christine ;

X = john
Y = sarah
Z = hugo ;

No
******************************************************
(defvar *gg4* (mk-goal-clause '((son james ?X ?Y))))

4 ?- son(james,X,Y).

X = peter
Y = jane

Yes
******************************************************
(defvar *gg5* (mk-goal-clause '((daughter christine ?X ?Y))))

5 ?- daughter(christine,X,Y).

X = john
Y = sarah

Yes
******************************************************
(defvar *gg6* (mk-goal-clause '((grandfather ?X ?Y))))

6 ?- grandfather(X,Y).

X = gerry
Y = james ;

X = gerry
Y = mike ;

X = gerry
Y = christine ;

X = gerry
Y = hugo ;

No
******************************************************
(defvar *gg7* (mk-goal-clause '((aunt ?X ?Y))))

7 ?- aunt(X,Y).

X = jane
Y = christine;

X = jane
Y = hugo ;

X = sarah
Y = james ;

X = sarah
Y = mike ;

No
******************************************************
(defvar *gg8* (mk-goal-clause '((uncle peter ?X))))

8 ?- uncle(peter,X).

X = christine;

X = hugo;

No
******************************************************
(defvar *gg9* (mk-goal-clause '((paternal-cousin ?X ?Y))))

9 ?- cousin(X,Y).

X = james
Y = christine ;

X = james
Y = hugo ;

X = mike
Y = christine ;

X = mike
Y = hugo;

X = christine
Y = james ;

X = christine
Y = mike ;

X = hugo
Y = james ;

X = hugo
Y = mike ;

No
******************************************************
(defvar *gg10* (mk-goal-clause '((paternal-ancestor ?X ?Y james))))

10 ?- ancestor(X,Y,james).

X = peter
Y = jane ;

X = gerry
Y = mary ;

|#


A Horn clause resolution theorem prover in Lisp

;;; A Horn-Clause Resolution Theorem Prover in Lisp:
;;; February 24th 2017 - March 16th 2017:   v. 1.0 -- initial release
;;;
;;; v. 1.01  March 18th 2017  -- remove state variable *goals* from show-proof, now functional
;;; ---
;;; [Update: (March 21st 2017): RTP release 1.1 is now available. See:
http://interweave-consulting.blogspot.co.uk/2017/03/improved-resolution-theorem-prover-rtp.html
;;; ---
;;; Based on code from From Peter Norvig's book: Chapter 11
;;; "Paradigms of Artificial Intelligence Programming" - initially.
;;;
;;; Unification, Prolog, Resolution, inference control strategies
;;; generation of all proofs, extraction of proofs.
;;;
;;; Posted here:
;
http://interweave-consulting.blogspot.co.uk/2017/03/a-horn-clause-resolution-theorem-prover.html
;;;
;;;  For documentation see here (you really need to read this first!):
;
; http://interweave-consulting.blogspot.co.uk/2017/03/description-theorem-prover-in-lisp.html
;;;
; (load  "C:\\Users\\HP Owner\\Google Drive\\Lisp\\Prog-RTP\\RTP.lisp")
;
;;; ----------------------------------------------------------------------
;;;
;;; Part 1: Unification
;;;
;;;  unify works on literals: eg (LIKES SALLY RENNER), (LIKES SALLY ?WHO)
;;;
;;;  --- Bindings: a list of dotted pairs created by unify: like this ---
;;;
;;;   ((?WHO . SALLY) (#:?X1113 . SALLY))

(defconstant +fail+ nil "Indicates unification failure")

(defconstant +no-bindings+ '((t . t))
"Indicates pat-match success but with no variables.")

(defun variable-p (x)    ; Symbol -> Bool
  "Is x a variable, a symbol beginning with '?'"
  (and (symbolp x) (equal (char (symbol-name x) 0) #\? )))

(defun get-binding (var bindings)
  "Find a (variable . value) pair in a binding list."
  (assoc var bindings))

(defun binding-val (binding)
  "Get the value part of a single binding."
  (cdr binding))

(defun lookup (var bindings)
  "Get the value part (for var) from a binding list."
  (binding-val (get-binding var bindings) ))

(defun extend-bindings (var val bindings)
  "Add a (var . value) pair to a binding list, remove (t . t)"
  (cons (cons var val) (if (equal bindings +no-bindings+) nil bindings)))

; --- Unification -------------------------------------------------------

(defparameter *occurs-check* t "Should we do the occurs check? If yes, t")

(defun unify (term-1 term-2 &optional (bindings +no-bindings+))
;  Lit x Lit -> Bindings
  "See if term-1 and term-2 match with given bindings"
  (cond ((equal bindings '+fail+) '+fail+)
        ((equal term-1 term-2) bindings)
        ((variable-p term-1) (unify-variable term-1 term-2 bindings))
        ((variable-p term-2) (unify-variable term-2 term-1 bindings))
        ((and (consp term-1) (consp term-2))
            (unify (rest term-1) (rest term-2)
                (unify (first term-1) (first term-2) bindings) ) )
        (t '+fail+) ) )

(defun unify-variable (var term bindings)     ; Var x Lit -> Bindings
  "Unify var with term, using (and maybe extending) bindings"
  (cond ((get-binding var bindings)
             (unify (lookup var bindings) term bindings))
        ((and (variable-p term) (get-binding term bindings))
             (unify var (lookup term bindings) bindings))
        ((and *occurs-check* (occurs-check var term bindings))
             '+fail+)
        (t (extend-bindings var term bindings))))

; > (unify '(likes sally renner) '(likes sally ?who)  +no-bindings+)
; ((?WHO . RENNER))

(defun occurs-check (var literal bindings)  ; Var x Lit -> Bool
  "Does var occur anywhere 'inside literal'? Returns t if it does (so fail)"
  (cond ((eq var literal) t)
        ((and (variable-p literal) (get-binding literal bindings))
         (occurs-check var (lookup literal bindings) bindings))
        ((consp literal) (or (occurs-check var (first literal) bindings)
                       (occurs-check var (rest literal) bindings)))
        (t nil)))

(defun unifier (literal literal-1)  ; ; Lit x Lit -> Lit
  "Return something that unifies with both literal and y (or +fail+)"
  (subst-bindings (unify literal literal-1) literal) )

(defun subst-bindings (bindings literal) ; Bindings x Lit ->Lit
  "Substitute the value of variables in bindings into literal,
taking recursively bound variables into account. Also works with clauses."
  (cond ((equal bindings '+fail+) '+fail+ )
        ((equal bindings +no-bindings+) literal)
        ((and (variable-p literal) (get-binding literal bindings))
              (subst-bindings bindings (lookup literal bindings) ))
        ((atom literal) literal)
        ( t (cons (subst-bindings bindings (car literal))
                        (subst-bindings bindings (cdr literal )) ) ) ) )

; --- Replace anonymous variables and rename variables in clause --------

(defun replace-?-vars (exp)
  "Replace any anonymous variable ? within exp with a var of the form ?123"
  (cond ((eq exp '?) (gensym "?"))
        ((atom exp) exp)
        (t (cons (replace-?-vars (first exp))
                 (replace-?-vars (rest exp))) ))  )

(defun rename-variables (x)       ; clause -> clause (with vars renamed)
  "Replace all variables in x with new ones"
  (sublis (mapcar #'(lambda (var) (cons var (gensym (string var))))
                  (variables-in x))
          x))

(defun variables-in (exp)
  "Return a list of all the variables in exp"
  (unique-find-anywhere-if #'variable-p exp))

(defun unique-find-anywhere-if (predicate tree &optional found-so-far)
  "Return a list of leaves of tree satisfying predicate,
    with duplicates removed"
  (if (atom tree)
      (if (funcall predicate tree) (adjoin tree found-so-far) found-so-far)
      (unique-find-anywhere-if predicate (first tree)
                (unique-find-anywhere-if predicate (rest tree) found-so-far)
 )))

;;; ----------------------------------------------------------------------
;;;
;;; Part 2: clauses and extended clauses
;;;
;;; --- Constants, variables and parameters ---

(defconstant <- nil   "pos/neg literals separator")
(defvar *axioms* nil)               ; list of all 'program' clauses
(defvar *goals* nil)                ; list of goal clauses

(defconstant +empty-clause+ t
    "indicates a proof: we resolved to the empty clause")
(defconstant +no-resolvant+ t
    "indicates clauses don't resolve")

; -----------------------------------------------------------------------
; EXAMPLE CLAUSES - WE HAVE AN EXTRA LEVEL OF PARENS FOR <-  .. REMEMBER!
;
; A fact is a clause (a list of literals) which has one (positive) literal
; followed by <- (which has value nil though this is not currently used).
; (defvar *c1* '( (likes horvath moties) <- )    ; a fact clause

; A rule is a clause (a list) which is a (positive) literal (the clause head)
; followed by <- and then a list of literals - the body of the clause.
;
; We use <- with value nil as a spacer only for human readability.
; (defvar *c2* '((likes sally ?who) <- ((likes ?who ?y) (likes ?y moties))) ;rule
;
; A goal is a clause (a list) of one or more negative literals.
; First element is <- for human readability.
; (defvar *g* '(<- ((likes ?x renner) (likes ?x rod)) ) )   ; a goal clause
;
; An index is a binary tree of integers, with leaves nil.
; Example: (1 (nil nil)) or (16 (12 (7 (nil nil)) (4 (nil nil)) ) (5 (nil nil)) )
; Each leading integer is the current clause number;
; the two immediate children are the two parent clauses .. and so on.
; Initial goals and axioms have no parents, thus nil.
;
; An extended clause is a triple: index,  clause then (if a goal) binding.
; Implemented as a list like this: (index clause binding). Example:
;
; (defvar *icb* '((13 (4 (nil nil)) (2 (nil nil)))             ; Index
;                      (<- ((likes ?x renner) (amusing ?x)))   ; Clause
;                               ((T . T))))                    ; Binding
;
; I don't use constructors/projectors for extended clauses:
; just remember their structure as triples.

; --- Clause constructors and projectors ---

(defun mk-fact-clause (literal)              ; Lit -> fact clause
   (list literal '<-))

(defun mk-rule-clause (literal literal-list) ; Lit x Lit-list ->rule clause
   (list literal '<- literal-list))

(defun mk-goal-clause (literal-list)         ; Lit-list -> goal clause
   (list '<- literal-list))

; --- test data (Mote in God's Eye): axioms and goal ---

(defvar *c1* (mk-fact-clause '(member ?item (?item . ?rest ))))
(defvar *c2* (mk-rule-clause '(member ?item (? . ?rest)) '((member ?item ?rest))))
(defvar *c3* (mk-fact-clause '(likes rod horvath)))
(defvar *c4* (mk-fact-clause '(likes sally renner)))
(defvar *c5* (mk-fact-clause '(likes sally rod)))
(defvar *c6* (mk-fact-clause '(likes hardy renner)))
(defvar *c7* (mk-fact-clause '(likes hardy rod)))
(defvar *c8* (mk-fact-clause '(amusing hardy)))
(defvar *c9* (mk-fact-clause '(likes horvath moties)))
(defvar *c10* (mk-rule-clause '(likes sally ?x) '((likes ?x moties)) ) )
(defvar *c11* (mk-rule-clause '(likes rod ?x) '((likes ?x renner) (likes ?x rod))))
(defvar *c12* (mk-rule-clause '(likes ?x ?y) '((amusing ?y) (likes rod ?y)) ) )
(defvar *c13* (mk-fact-clause '(likes ?x ?x)))

(defvar *g1* (mk-goal-clause '((likes sally ?who))))
(defvar *g2* (mk-goal-clause '((member sally (rod renner horvath sally . moties)))))

(setf *axioms* (list *c1* *c2* *c3* *c4* *c5* *c6* *c7* *c8*
                 *c9* *c10* *c11* *c12* *c13*))

(setf *goals* (list *g1*))

; -----Datatype operators for clauses -----------------------------------

(defun is-fact-clause (clause)
   (and (= (length clause) 2) (equal (cadr clause) '<-)) )

(defun is-rule-clause (clause)
   (and (= (length clause) 3) (equal (cadr clause) '<-)) )

(defun is-goal-clause (clause)
   (and (= (length clause) 2) (equal (car clause) '<-)) )

(defun axiom-head-literal (clause)           ; Clause -> Lit (remove <-)
    (if (or (is-fact-clause clause) (is-rule-clause clause))
        (first clause)
        "error - not a fact or rule clause" ) )

(defun axiom-body-literal-list (clause)      ; Clause -> Lit-list (remove <-)
    (if (is-rule-clause clause) (third clause) nil))

(defun goal-literal-list (goal-clause)    ; Clause -> Lit-list (remove <-)
    (if (is-goal-clause goal-clause)
            (second goal-clause)
            "error - not goal clause"))

(defun pred (literal) (car literal))    ; Lit -> Symbol (predicate)

; ----------------------------------------------------------------------
#|
; get-clauses: Pred-symbol x Clause-list -> Clause-list where head matches
; This is an optimisation not currently used.

(defun get-clauses (p cl)
  "Get those clauses (facts and rules) from cl (the kb) which match
   the (goal) predicate, and which are therefore candidates for unification"
  (remove-if-not #'(lambda (c) (equalp p (pred (axiom-head-literal c)))) cl) )
|#

; initialise-databases: Clause-list x Clause-list -> Extended-Clause versions
; note - args are clause lists (from user), not extended clauses

(defun initialise-databases (goal-list axiom-list)  
   "Takes the goal and the program and creates extended clause list versions"
  (let* ((index     (list 0 (list nil nil)))
         (ia-list   (mk-extended-clauses index axiom-list nil))
         (new-index (list (apply #'max (mapcar #'caar ia-list))(list nil nil)))
         (igb-list  (mk-extended-clauses new-index goal-list +no-bindings+)))
      (list igb-list ia-list) ) )

(defun mk-extended-clauses (index clause-list bindings) ; -> ig(b)-list
  (cond ((null clause-list) nil)
         (bindings (let ((index1 (incr-index index)) )
                     (cons (list index1 (car clause-list) bindings)  ; goal list
                        (mk-extended-clauses index1 (cdr clause-list) bindings))))
         (t     (let ((index1 (incr-index index)) )
                   (cons (list index1 (car clause-list))           ; axiom list
                      (mk-extended-clauses index1 (cdr clause-list) bindings))))))

(defun incr-index (i) (list (+ (car i) 1) (cadr i)) ) ; Just ups the first number

;   (incr-index '(19 ((17 ((14 (nil nil)) (10 (nil nil))))
;   (20 ((17 ((14 (nil nil)) (10 (nil nil)))

;;; ----------------------------------------------------------------------
;;;
;;;   Part 3: the theorem prover
;;;
;;;  ---  Binary Resolution
;;;
;;;   L1 <= M1,M2,M3      <= L1,G2
;;;   --------------------------------------------   L1 is resolved upon giving binding b
;;;          <= G2,M1,M2,M3                         The binding b is applied to the new goals
;;;

;  binary-resolve: Goal x Axiom x Bindings -> new-Goal x Bindings (after substs)
;  note that these are all clauses, not extended clauses

(defun binary-resolve (goal axiom1 b1)
  "goal =  a goal clause (previously extracted from extended-goal-list)
    axiom = a fact or rule clause (extracted from the extended-axiom-list)  
    b1 =    bindings stored with the goal clause"
  (let* ((axiom                (rename-variables axiom1)) ;rename vars in axiom
         (axiom-head-lit       (axiom-head-literal axiom))       ; remove '<-
         (axiom-body-lit-list  (axiom-body-literal-list axiom))  ; remove '<-
         (goal-lit-list        (goal-literal-list goal))         ; remove '<-
         (head-goal-lit        (car goal-lit-list))
         (other-goal-lits      (cdr goal-lit-list))
         (b                    (unify axiom-head-lit head-goal-lit b1)) )
    (cond ((equal b '+fail+)
           (list '+no-resolvant+ '+fail+))
          ( t (if (and (null axiom-body-lit-list) (null other-goal-lits))
                  (list '+empty-clause+ b)
                (list (mk-goal-clause
                       (mapcar #'(lambda (literal)
                                   (subst-bindings b literal))
                               (append other-goal-lits axiom-body-lit-list) ))
                      b))))) )

; Example:
;  (binary-resolve  *g1*  *c12* +no-bindings+)
;  ((<- ((AMUSING ?WHO) (LIKES ROD ?WHO))) ((#:?Y871 . ?WHO) (#:?X870 . SALLY)))

;  one-step-prove:  Nat x ext-goal-list x axioms -> ext-goal-list
(defun one-step-prove (max-i igb-list ia-list)
  "Takes max index so far,  extended goal list,
   returns new extended goal list, (no +fail+s)"
  (let* ((igb       (car igb-list))   ; igb = extended goal clause, head of list
         (g-index   (first igb))      ; extract the goal clause index
         (goal      (second igb))     ; extract the goal clause itself
         (b1        (third igb))      ; extract the previously stored binding
         (a-indexes (mapcar #'first  ia-list))   ; list of indexes of axioms
         (a-list    (mapcar #'second ia-list))   ; list of axiom clauses
         (new-gb-list (mapcar #'(lambda (x) (binary-resolve goal x b1)) a-list)) )
    (mk-new-igb-list max-i g-index a-indexes new-gb-list) ) )

; Example:
; A detailed walkthrough of one-step-prove starting with the arguments ----

(defvar *igb-list-ia-list* (initialise-databases *goals* *axioms*))
(defvar *igb-list* (car *igb-list-ia-list*))
(defvar *ia-list* (cadr *igb-list-ia-list*))


;    *igb-list*                                           ; extended goals
; (((14 (nil nil)) (<- ((LIKES SALLY ?WHO))) ((T . T))))
;
;     (pprint *ia-list*)                                  ; extended axioms
#|
(((1 (NIL NIL)) ((MEMBER ?ITEM (?ITEM . ?REST)) <-))
 ((2 (NIL NIL)) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
 ((3 (NIL NIL)) ((LIKES ROD HORVATH) <-))
 ((4 (NIL NIL)) ((LIKES SALLY RENNER) <-))
 ((5 (NIL NIL)) ((LIKES SALLY ROD) <-))
 ((6 (NIL NIL)) ((LIKES HARDY RENNER) <-))
 ((7 (NIL NIL)) ((LIKES HARDY ROD) <-))
 ((8 (NIL NIL)) ((AMUSING HARDY) <-))
 ((9 (NIL NIL)) ((LIKES HORVATH MOTIES) <-))
 ((10 (NIL NIL)) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
 ((11 (NIL NIL)) ((LIKES ROD ?X) <- ((LIKES ?X RENNER) (LIKES ?X ROD))))
 ((12 (NIL NIL)) ((LIKES ?X ?Y) <- ((AMUSING ?Y) (LIKES ROD ?Y))))
 ((13 (NIL NIL)) ((LIKES ?X ?X) <-)))
|#
;
;    (setf igb (car *igb-list*))    ; curr extended goal clause
; ((14 (NIL NIL)) (<- ((LIKES SALLY ?WHO))) ((T . T)))
;
;    (setf g-index (first igb))
; (14 (NIL NIL))
;
;    (setf goal (second igb))
; (<- ((LIKES SALLY ?WHO)))
;
;    (setf b1 (third igb))
; ((T . T))
;
;    (pprint (setf a-indexes (mapcar #'first  *ia-list*)) )
#|
((1 (NIL NIL))
 (2 (NIL NIL))
 (3 (NIL NIL))
 (4 (NIL NIL))
 (5 (NIL NIL))
 (6 (NIL NIL))
 (7 (NIL NIL))
 (8 (NIL NIL))
 (9 (NIL NIL))
 (10 (NIL NIL))
 (11 (NIL NIL))
 (12 (NIL NIL))
 (13 (NIL NIL)))
|#
;
;    (pprint (setf a-list (mapcar #'second *ia-list*)))
#|
(((MEMBER ?ITEM (?ITEM . ?REST)) <-)
 ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST)))
 ((LIKES ROD HORVATH) <-)
 ((LIKES SALLY RENNER) <-)
 ((LIKES SALLY ROD) <-)
 ((LIKES HARDY RENNER) <-)
 ((LIKES HARDY ROD) <-)
 ((AMUSING HARDY) <-)
 ((LIKES HORVATH MOTIES) <-)
 ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
 ((LIKES ROD ?X) <- ((LIKES ?X RENNER) (LIKES ?X ROD)))
 ((LIKES ?X ?Y) <- ((AMUSING ?Y) (LIKES ROD ?Y)))
 ((LIKES ?X ?X) <-))
|#
;
; - one-step-prove maps binary-resolve across axioms -> resolvants (if any):
;
; (pprint (setf new-gb-list (mapcar #'(lambda (x) (binary-resolve goal x b1)) a-list)))
;
#|
((+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+EMPTY-CLAUSE+ ((?WHO . RENNER)))
 (+EMPTY-CLAUSE+ ((?WHO . ROD)))
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 (+NO-RESOLVANT+ +FAIL+)
 ((<- (#)) ((#:?X1003 . ?WHO)))
 (+NO-RESOLVANT+ +FAIL+)
 ((<- (# #)) ((#:?Y1006 . ?WHO) (#:?X1005 . SALLY)))
 (+EMPTY-CLAUSE+ ((?WHO . SALLY) (#:?X1007 . SALLY))))
|#

; and finally we remove the +FAIL+ values and update the clause indexes for the
; genuine new clauses - to return the list of additional igb clauses.
;
; That's the job of mk-new-igb-list.
;
;   (setf new-igb-list1 (mk-new-igb-list 14 g-index a-indexes new-gb-list) ))
;   (mapcar #'pprint new-igb-list1)
#|
((15 ((14 (NIL NIL)) (4 (NIL NIL)))) +EMPTY-CLAUSE+
     ((?WHO . RENNER)))
((16 ((14 (NIL NIL)) (5 (NIL NIL)))) +EMPTY-CLAUSE+
     ((?WHO . ROD)))
((17 ((14 (NIL NIL)) (10 (NIL NIL)))) (<- ((LIKES ?WHO MOTIES)))
     ((#:?X1003 . ?WHO)))
((18 ((14 (NIL NIL)) (12 (NIL NIL)))) (<- ((AMUSING ?WHO) (LIKES ROD ?WHO)))
     ((#:?Y1006 . ?WHO) (#:?X1005 . SALLY)))
((19 ((14 (NIL NIL)) (13 (NIL NIL)))) +EMPTY-CLAUSE+
      ((?WHO . SALLY) (#:?X1007 . SALLY)))


|#
;
; mk-new-igb-list: max-index x g-index x a-indexes x new-gb-list -> igb-list
; Read as 'make additional igb extended clauses' - to be added to the pot
; Takes the new resolvants from the latest goal and creates additional igb
; extended clauses to be added to the overall igb-list.

; mk-new-igb-list arguments:
; max-i is just a number, the highest clause number yet allocated, eg 7
; a-index: eg (3 (nil nil))
; g-index: eg  (15 ((3 (nil nil)) (2 (nil nil))))
; a-indexes: eg ((1 (nil nil)) (2 (nil nil)) ...  (n (nil nil)) )
; new-gb-list: eg ((+no-resolvant+ +fail+) (goal b1) (+empty-clause+ b2) ..)
; the task here is to remove +fail+s and update the indexes.

(defun mk-new-igb-list (max-i g-index a-indexes new-gb-list)
  (if (null new-gb-list)
      nil
    (let* ((a-index        (car a-indexes))  ;(i (nil nil)) index for axiom
           (a-rest-indexes (cdr a-indexes))  ;remaining axiom indexes
           (gb             (car new-gb-list))
           (gb-rest        (cdr new-gb-list))
           (g              (first  gb))  
           (b              (second gb)) )
      (cond ((equal b '+fail+)
                (mk-new-igb-list max-i g-index a-rest-indexes gb-rest))
            (t  (let ((new-index (list (+ max-i 1) (list g-index a-index))))
                  (cons (list new-index g b)
                        (mk-new-igb-list (+ max-i 1) g-index
                                          a-rest-indexes gb-rest))))))))


;   (pprint (setf new-igb-list (one-step-prove 14 *igb-list* *ia-list*)))
;
; [Same result as from (mapcar #'pprint new-igb-list1) above].

;;; -- Now we look to the top-level loop which iterates until termination --

(defvar *1step* t)  ; If t stops proof loop each iteration and
;                          prints archived-proofs & goals

(defun empty-clause-p (igb-clause)              ;  -> Bool
   (equal '+empty-clause+ (second igb-clause)))

(defun prove1 (archived-goals archived-proofs igb-list ia-list depth)
 ; -> archived-proofs
  "'prove1' iterates, finally returning archived-goals and archived-proofs
   for subsequent proof extraction"
  (if (or (zerop depth) (null igb-list))
      (if *1step* (progn (terpri)
                         (princ "Done: archived-goals = ")
                         (pprint archived-goals) (terpri)
                         (princ "Archived-proofs = ")
                         (pprint archived-proofs) (terpri)
                         (list archived-goals archived-proofs))
                   (list archived-goals archived-proofs))
    (let* ((max-i (apply #'max (mapcar 'caar (append archived-proofs igb-list))))
           (new-igb-list1     (one-step-prove max-i igb-list ia-list))
           (new-empty-clauses (remove-if-not #'empty-clause-p new-igb-list1))
           (new-igb-list      (remove-if #'empty-clause-p new-igb-list1))
           (archived-goals1   (cons (car igb-list) archived-goals))
           (archived-proofs1  (append new-empty-clauses archived-proofs))
           (igb-list1         (cdr igb-list))
           (next-igb-list     (append igb-list1 new-igb-list)) )
           ; depth first: reverse append order for breadth first
       (if *1step* (progn (terpri)
                          (princ "Depth = ") (princ depth)
                          (princ ". Archived-goals1 = ")
                          (pprint archived-goals1) (terpri) (terpri)
                          (princ "Archived-proofs1 = ")
                          (pprint archived-proofs1) (terpri) (terpri)
                          (princ "next-igb-list = ")
                          (pprint next-igb-list)  (terpri)
                          (princ "type return: ") (terpri)
                          (read-char) (princ "-----") ))
      (prove1 archived-goals1 archived-proofs1
                  next-igb-list ia-list (- depth 1)))))

(defun prove (goals axioms depth) ;goals and axioms are input clause-lists
  "prove turns initial clauses into extended-clauses then calls prove1.
   Returns a 2 member list of extended clauses:(archived-goals archived-proofs)"
   (let* ((igb-ia (initialise-databases goals axioms))
          (igb-list (first igb-ia))
          (ia-list (second igb-ia))
          (initial-archived-goals  nil)
          (initial-archived-proofs nil) )
     (prove1 initial-archived-goals initial-archived-proofs igb-list ia-list depth)))

; 'archived-proofs' is a list of igb extended clauses
; (setf *archived-proofs* (prove *goals* *axioms* 4))
;
; --- Transform archived-proofs into a readable collection of proofs --
; Note that 'archived-goals-and-proofs' =  a two-member list:
;     (archived-goals archived-proofs)
; is returned by 'prove'.

(defun show-all-proofs (archived-goals-and-proofs ia-list goals)
  (let* ((archived-goals  (first  archived-goals-and-proofs))
         (archived-proofs (second archived-goals-and-proofs))
         (all-igbs  (append archived-goals archived-proofs ia-list))
         (proofs (mapcar #'(lambda (x) (show-proof x all-igbs goals))
                              archived-proofs)))
     (reverse proofs)))

(defun show-proof (empty-igb all-igbs top-level-goals)
 "empty-igb is the root of the proof tree we construct here"
       (let* ((index     (first empty-igb))
              (answer    (subst-bindings (third empty-igb) top-level-goals))
              (proof     (mk-proof-list index all-igbs)) )
          (list answer (reverse proof))) )

(defun mk-proof-list (i all-igbs)
  "Traverses index i as a tree pulling out the matching clauses"
   (if (null i)
        nil
      (let* ((current-igb-# (first i))
             (current-igb (get-igb-by-n current-igb-# all-igbs))
             (current-clause (second current-igb))
             (left-ancestor  (first (second i)))
             (right-ancestor (second (second i)))
             (tg (list (car i) (first (first (second i)))
                               (first (second (second i))))))
         (cons (list tg current-clause)
               (append (mk-proof-list left-ancestor  all-igbs)
                       (mk-proof-list right-ancestor all-igbs) ))) ) )

(defun get-igb-by-n (n igb-list)  ; nat x igb-list -> igb
  " example (n=3) returns ((3 (nil nil)) ((LIKES ROD HORVATH) <-)) "
   (find-if #'(lambda (igb) (= n (caar igb))) igb-list))


;;; ----------------------------------------------------------------------
;;;
;;;  Part 4:  TEST DATA

#|

With goal: (setf *goals* (list *g1*))

   ((<- ((LIKES SALLY ?WHO))))

   (defvar *igb-list-ia-list* (initialise-databases *goals* *axioms*))
   (defvar *igb-list* (car *igb-list-ia-list*))  ; ext. goal clause(s)
   (defvar *ia-list* (cadr *igb-list-ia-list*))  ; ext. axiom clauses

; The above three assignments were eval'ed above so already bound.
; Prove itself calls 'initialise-databases' to set up extended clauses

 (setf archived-goals-and-proofs (prove *goals* *axioms* 6))   ; depth 6 here

(pprint (setf all-proofs (show-all-proofs archived-goals-and-proofs *ia-list* *goals*)))

Result: (with a few added line-breaks)

((((<- ((LIKES SALLY SALLY))))
  (((13 NIL NIL) ((LIKES ?X ?X) <-))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((19 14 13) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY ROD))))
  (((5 NIL NIL) ((LIKES SALLY ROD) <-))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((16 14 5) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY RENNER))))
  (((4 NIL NIL) ((LIKES SALLY RENNER) <-))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((15 14 4) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY MOTIES))))
  (((13 NIL NIL) ((LIKES ?X ?X) <-))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((17 14 10) (<- ((LIKES ?WHO MOTIES))))
   ((24 17 13) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY HORVATH))))
  (((9 NIL NIL) ((LIKES HORVATH MOTIES) <-))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((17 14 10) (<- ((LIKES ?WHO MOTIES))))
   ((20 17 9) +EMPTY-CLAUSE+)))

 (((<- ((LIKES SALLY SALLY))))
  (((13 NIL NIL) ((LIKES ?X ?X) <-))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((10 NIL NIL) ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES))))
   ((14 NIL NIL) (<- ((LIKES SALLY ?WHO))))
   ((17 14 10) (<- ((LIKES ?WHO MOTIES))))
   ((21 17 10) (<- ((LIKES MOTIES MOTIES))))
   ((27 21 13) +EMPTY-CLAUSE+))))

; -------------------------------------------------------------------------

With goal: (setf *goals* (list *g2*))

   ((<- ((MEMBER SALLY (ROD RENNER HORVATH SALLY . MOTIES)))))


(pprint (setf all-proofs (show-all-proofs archived-goals-and-proofs *ia-list* *goals*)))

((((<- ((MEMBER SALLY (ROD RENNER HORVATH SALLY . MOTIES)))))
  (((1 NIL NIL) ((MEMBER ?ITEM (?ITEM . ?REST)) <-))
   ((2 NIL NIL) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
   ((2 NIL NIL) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
   ((2 NIL NIL) ((MEMBER ?ITEM (? . ?REST)) <- ((MEMBER ?ITEM ?REST))))
   ((14 NIL NIL) (<- ((MEMBER SALLY (ROD RENNER HORVATH SALLY . MOTIES)))))
   ((15 14 2) (<- ((MEMBER SALLY (RENNER HORVATH SALLY . MOTIES)))))
   ((16 15 2) (<- ((MEMBER SALLY (HORVATH SALLY . MOTIES)))))
   ((17 16 2) (<- ((MEMBER SALLY (SALLY . MOTIES)))))
   ((18 17 1) +EMPTY-CLAUSE+))))

|#

; --------------------------- End of program -------------------------------