11) An Outline of Bit-Crunching Theorem Prover "Iphigenia"

 

(*) named after my mother, the late Iphigenia Stathis (Maths teacher), who died in 1998.

 

 

 

·                The material that follows is of highly technical nature, but I re-wrote it recently, to make it as simple as possible, suitable for general distribution to a variety of audiences (or… possible employers). It concerns theorem-proving for Expert Systems, but done in a strange way that is extremely simple, elegant and parallel (in the required computations). It is all based on the three Axioms of Multiple Form Logic™.

 

 

 

11.1) An example of the Algorithm’s operation:

 

Consider the following type of logic expression: A and B and C and ... =>  a or b or c ...

 

In "Multiple Form Logic", this translates to:  (A#1, B#1, C#1, ... )#1#1, a , b , c , ...

 

i.e. A#1, B#1, C#1, ...  a , b , c , ...  (by Axiom 2, X#1#1=X)

 

Suppose now that our set of (logic) variables is finite (so that it can be encoded in bits). For purposes of clear understanding, consider (for the moment) a system with eight variables:

 

A,B,C,D,E,F,G,H

 

For example, consider the following "logic system" containing these variables:

 

B and C => H

E and F => C or D

C => E or F

B => F

D => B

D => C

E => C or F                   (where, all the statements are assumed to be “AND-ed together”)

 

 

Consider now a "logic query" (for "evaluation"):

 

D => H   ...which turns the whole system, in Multiple Form Logic:

 

 

(B#1, C#1, H)#1,

(E#1, F#1, C, D)#1,

(C#1, E , F)#1,

(B#1, F)#1,

(D#1, B)#1,

(D#1, C)#1,

(E#1, C , F)#1,

D#1, H.

 

We can now easily get successive simplifications of this system (by applying the Three Axioms):

 

 

(B#1, C#1, H)#1, (E#1, F#1, C, D)#1, (C#1, E , F)#1, (B#1, F)#1, (D#1, B)#1, (D#1, C)#1, (E#1, C , F)#1, D#1, H

(B#1, C#1)#1, (E#1, F#1, C, D)#1, (C#1, E , F)#1, (B#1, F)#1, B#1, C#1, (E#1, C , F)#1, D#1, H

1, (E#1, F#1, C, D)#1, (C#1, E , F)#1, (B#1, F)#1, B#1, C#1, (E#1, C , F)#1, D#1, H

1  (TRUE)

 

 

We can take advantage of bit-encoding, if we represent such systems by arrays of bits. A system like this can be represented by a "bit-array" with a left-hand side (“assumptions”) and a right-hand side (“consequences”),  where each “fact row” is a set of “AND-ed assumptions” and a set of “OR-ed consequences” (XORed with 1):

 

 

For example, the (previous) system:

 

(B#1, C#1, H)#1,

(E#1, F#1, C, D)#1,

(C#1, E , F)#1,

(B#1, F)#1,

(D#1, B)#1,

(D#1, C)#1,

(E#1, C , F)#1,

D#1, H

 

...can be encoded as follows:

 

 

 

 

 

11.2) Rule of Vertical Cancelation (RVC):

 

The bit-representations help us automate and simplify further the reductions. First of all, notice that (because of Axiom 3) we can reset (to zero) all the bits in every column which correspond to One-bits in the “query row”, since the query row is on the Outer Space of the fact rows (so Outer from Inner can be cancelled –Axiom 3):

 

 

 

The first stage of simplifications resets all the “fact row bits” that correspond to the fourth position of the left-hand-side of the query and the eighth position of the right-hand-side of the query. The resulting bit-table is:

 

 

 

11.3) Rule of Diagonal Transfer (RDT):

 

The next step is very interesting: Notice that there are now two rows which contain a single bit. Since these have become “Outer” in relation to the (“inner”) fact rows, i.e. they behave “as if” they are already a part of the (outer) query row, they can be transferred “diagonally” to the query row at the bottom :

 

 

Evidently, the (striken-through-) deleted rows correspond to terms B#1, C#1, which are now "outside" the rest of the system, i.e. they can now be safely assumed to co-exist with the query row. Therefore, we can "transfer" these rows to the bottom “fact-row "diagonally", in a way that makes the fact-row OR-ed with the new terms:

 

We can now repeat the first stage, using the Rule of Vertical Cancelation (RVC), i.e. reset all bits in relevant columns for which the corresponding bit of the bottom line (the "query row") has recently become "1":

 

 

 

 

i.e.

 

 

Notice now that the first line in this system has become zeroed completely. This means that the system contains an isolated "1", or-ed with other terms.

 

Therefore, by axiom 1 the entire system has becomes "1" or "TRUE".

 

I.e. the answer to the logic query (“D => H”) is “YES”!

 

This is a simplification process for systems of logical formulae of the form described in the beginning, which are Rules for a class of Expert Systems (at the moment, using only propositional logic). Now, there are a few more things required, to build a complete Expert-System Query Evaluation Engine, in Multiple Form Logic™:

 

 

11.4) Fact-Row Extinction of type 1 (FRE-1):

 

Firstly, if a bit-position in the left-hand-side (of any fact-row) is One, and the corresponding bit-position in the right-hand-side (of the same fact-row) is also One, then we can safely discard this fact-row completely, since it is equal to (X#1,X)#1, which (by Theorem T4) is void!   I.e. fact-rows like:

 

00010000 00010000    (where the fourth position bits are both one)

   ^        ^

01000000 01000000    (where the second position bits are both one)

 ^        ^

...can be discarded (erased totally, "as if they never existed")!

 

 

11.5) Fact-Row Extinction of type 2 (FRE-2):

 

Secondly, if a particular bit in the "right hand side of the query row" is One, and the corresponding bit in the "left hand side of a fact row" is also One, we can again erase this fact row, "as if it never existed":

 

XXXXXXXX XXXXXXXX

00010000 ........ ("fact row", with 4^th bit in the left-hand-side = 1)

XXXXXXXX XXXXXXXX

=================

........ 00010000 ("query row", with 4th bit in the right-hand-side = 1)

 

=>

 

XXXXXXXX XXXXXXXX

----------------- ("fact row"- erased now!)

XXXXXXXX XXXXXXXX

=================

........ 00010000 ("query row", with 4th right-side-bit = 1)

 

 

This is because the "fact row" is: (.... X#1... ....)#1 and the "query row" is  (........... ....X.....)  and we can "insert" X into ...X#1... (by Axiom 3) , to get X#X#1, which (by Axiom 2) is "1". If we also notice the "#1" on the right of each fact-row, then we see that the entire "fact row" becomes "1#1", which (by axiom 2, again) becomes void.

 

 

11.6) Fact-Row Extinction of type 3 (FRE-3):

 

An exactly similar process of simplification can take place in the opposite (diagonal) direction:  If the Query Row has a "1" in position N (leftwards) and there is a "Fact Row" which also has a "1" in the same position N (but rightwards), then this "Fact Row" can be safely discarded "as if it never existed".

 

This operation completes the list of very simple parallel bit-operations which are required, to simplify bit-encoded Expert System knowledge bases.

 

 

 

Finally, notice that everything described so far, refers to processes that can take place completely in parallel.