Infere - forward Inference Engine (on LISP)

I've finally concluded the first version of my forward inference engine, which I named Infere, ie "capable of doing inference", in english. I started this project, from bare ground, just 2 weeks ago, of which only the last 6 nights were really profitable, having me working an average of 6 hours on 24 possible. It might not seem much, but I am a strange creature, that can't handle too much of the same thing, for too long.

During Infere's first week, I faced several implementation difficulties, due to a very wrong approach to the problem. I first tried to allow the final user to write knowledge on natural language, and then I would parse the [english] sentences, correctly identifying which identifiers were variables, constants, functions, predicates, logical operators and quantifiers... That easily became an impossible task for a 2 weeks budget, and after many nightmares, I was wise to quit and focus on the inference algorithms, forcing the user to write stuff, according to a representation I had decided to support.

Infere is somewhat more sophisticated than the average inference engine, as it can treat existential and universal quantifications, automatic translation to Horn's form, generate all knowledge from a a set of formulas, and be used to demonstrate stuff.

For example, it can treat expressions like:

all x thinks (x) => exists (x)

which says that everything that thinks, exists...

or like

exists y loves_me (y)

which says that there is someone who loves me! Of course Infere can work with any other valid expressions built using the usual logical operators, like AND, OR, NOT and IMPLIES.

The algorithms for the inference procedure work on knowledge written on the Horn's form, which basically means that formulas must be expressed like ANDs of ORs. In order to work with such representation, Infere implements a translator.

For the example above, formulas can be written like [Horn's form]:

{not (thinks (x)) , exists (x)}

{loves_me (martina_hingis)}

These 2 formulas correspond to a knowledge base [KB], which Infere can use to breed new formulas. Don't get weird with the 2nd translation: the translation algorithms is such that one of its steps [step 5] says that you can cut the existential quantifier out of a clause, if the variable is not under the shadow of a universal quantifier - as it is the case - replacing it with some never used constant: I choose Martina Hingis!, and I wonder if she is the one who loves me :) :

#1 - get rid of implies [using a =>b == (not (a)) or b]

#2 - apply nots [for example (not (a or b)) == (not (a)) and (not (b))]

...

#5 - get rid of existential quantifiers, by replacing then with new constants, when the quantifier's variable is not under the shadow of any universal quantifier.

Of course that all this makes sense - for example, for the 2nd clause, if it exists someone who loves me, then we just give it a name; and for the 1st clause, if everyone who thinks, exists, then it is true that everything or exists, or doesn't think :)

Surely this might read strange to those who never used logic in a formal way, but this really is the way things are!

Yeah, yeah, but what's the point in translating logical stuff to Horn's form? Well, Horn's form is just a convenient representation for the inference algorithm to work on. The inference algorithm is rather simple, and so very beautiful. It just goes like this:

#1 - choose some proposition and look for its negation, somewhere, in other clause, in KB.

#2 - Find, if possible, a valid unification between the propositions, ie a way of turning one into the other. When and if done, insert into the KB the NEW clause that results from the unification - that clause should look like one of the previously used clauses, without the proposition whose negation was found.

#3 - If at some point you can generate an empty clause, that means your KB had contradicting stuff. If you can't generate new knowledge from some state on, it means that the KB has no contradictions.

Strangely, it is the case where you generate the empty clause that matters. Check the following example, taken from the OUTPUT of Infere!

Infere has its interface written in european portuguese, so if you don't know the language, the following translations will help you understand the nice example:

CAO is DOG ; SALIVA is SALIVATES ; INÍCIO DA INFERÊNCIA is INFERENCE BEGINS ; ITERACAO is ITERATION ; NOVA CLÁUSULA is NEW CLAUSE ; Substituições is Substs ; KB inconsistente is KB inconsistent ; a cláusula representa uma falsidade is the clause is false.

This example shows the inference engine working to demonstrate that if all dogs salivate, and if pluto is a dog, then it can't be that pluto does not salivate. The conclusion is reached by obtaining the empty clause, in a way called resolution ad absurdum... I think... my latin is as good as my japanese :)

Oh, here it is the example:

> (infere "kb.txt")

FORMULA #1= (ALL X1 (IMPLIES (CAO X1) (SALIVA X1)))

FORMULA #2= (CAO PLUTO) FORMULA #3= (NOT (SALIVA PLUTO))

INÍCIO DA INFERÊNCIA...

ITERACAO #1_________

CLÁUSULA #1: ((NOT (CAO VAR0)) (SALIVA VAR0))

CLÁUSULA #2: ((CAO PLUTO)) CLÁUSULA #3: ((NOT (SALIVA PLUTO)))

NOVA CLÁUSULA!! => ORIGEM: (1 , 2)

CLÁUSULA= ((SALIVA PLUTO))

Substituições: VAR0 / PLUTO ;

NOVA CLÁUSULA!! => ORIGEM: (1 , 3)

CLÁUSULA= ((NOT (CAO PLUTO)))

Substituições: VAR0 / PLUTO ;

ITERACAO #2_________

CLÁUSULA #1: ((NOT (CAO VAR0)) (SALIVA VAR0))

CLÁUSULA #2: ((CAO PLUTO))

CLÁUSULA #3: ((NOT (SALIVA PLUTO)))

CLÁUSULA #4: ((SALIVA PLUTO))

CLÁUSULA #5: ((NOT (CAO PLUTO)))

NOVA CLÁUSULA!! => ORIGEM: (5 , 2)

CLÁUSULA= NIL Substituições:

KB inconsistente!! => a cláusula representa uma FALSIDADE.