Some plans as to the work with Shen

[Antti Ylikoski]

There is something that I plan to attempt to submit to the SP

system.  If it will be good or not, remains to be seen.

I have been working on the Shen resolution algorithm.  See

https://en.wikipedia.org/wiki/Resolution_(logic)

The basic resolution is what I would characterize as a variant of the

breadth first search, resolve everything with everything else.

Potentially better resolution strategies exist.  I found in one

textbook the combination of the Set of Support and the Unit Preference

strategies:

See George F Luger: ARTIFICIAL INTELLIGENCE, 6th Edition, Pearson

International, ISBN 978-0-13-209001-8 Part V Chapter 14.2 Resolution

Theorem Proving pp. 582 -- in particular p. 597 "The unit preference

strategy along with the set of support can produce a more efficient

complete strategy".

As I write this, I have been delving into the well-known textbook by

Chang-Lee, and I wonder if I could create something useful from the

semantic resolution and the lock resolution in the Chang-Lee book.

We shall see if I can produce anything useful.

yours, AJY

Helsinki, Finland, the EU