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.

 

 

 

On the other hand, if our system does not reach this point, but appears to become stable (after a "round of bit-operations"), we can assume that it has been "minimised with respect to the particular query". In other words, the query was (again) answered, but answered "relatively" (to the knowledge base) with a "relative answer".

 

·                NOTE: If you wish, you can also download a piece of software that demonstrates the operation of this algorithm graphically, with text-mode graphics. (More details at the end of this section)

 

What follows is another example, to elucidate the operation of this algorithm more clearly.

E.g. suppose we assume that

 

(1) "To be Cretan”, implies "to be a lier",

(2) "To be a lier”, implies "to be a sinner",

(3) "To be a sinner", implies "to go to hell"

 

Here we have 4 variables (Cretan, lier, sinner, going-to-hell). First, We "bit-encode" these three expressions to:

 

1000 0100

0100 0010

0010 0001

 

OK. Now we are ready to "evaluate queries".

 

Suppose our first query is just one term: "to be a Cretan, implies to go to hell".

 

This can be bit-encoded to:

 

1000 0001

 

The system can now be progressively simplified "in parallel", to evaluate our Logical Query:

 

1000 0100

0100 0010

0010 0001

=========

1000 0001

 

...which becomes (by the "Rule of Vertical Cancellation"):

 

0000 0100 ß isolated bit, on the right

0100 0010

0010 0000

=========

1000 0001

 

 

By copying "diagonally" the isolated bit to the left-hand side of the query-line, we get ready for the next round of “Vertical Cancellations (RVC)”:

 

0100 0010

0010 0000

=========

1100 0001 ß bit 2 on the left has been "copied diagonally")

 

 

which is (by application of the "Rule of Vertical Cancellation"):

 

 

0000 0010 ß isolated bit, on the right

0010 0000

=========

1100 0001

 

 

By copying "diagonally" the isolated bit to the left-hand side of the query-line, we get:

 

0010 0000

=========

1100 0001

0010      ß isolated bit, copied “diagonally” to the left

 

i.e.

 

0010 0000

=========

1110 0001

 

 

which is (by application of the "Rule of Vertical Cancellation (RVC)"):

 

0000 0000 ß empty fact-row

=========

1110 0001

 

Now: Since the system contains one empty row (of zero bits only), the correspondig term is "1", i.e. "TRUE".

 

So, the answer to our query (“Does being Cretan imply going to hell”), is “YES”. ;-)      (see PS, at the end…)

 

 

 

11.7) A Demo-Program you can download:

 

 

When you run the program “bitprover.exe”, you will be asked to pick an existing Knowledge Base of Rules. (There is one such file, but you can edit it and re-save it under different names). The first argument in all the clauses r/3, q/3 is the internal example-number (the unique set of logic expressions to simplify). The clause r(n,…) is the “result clause” in the knowledge-base, or the “query row” (if you prefer). The q(n,…) clauses are the “fact rows”. The syntax of all these clauses is very simple: Arguments 2 and 3 are assumptions and conclusions respectively, “string lists” in PDC/Visual Prolog, i.e. statements enclosed in inverted commas, separated by commas and encapsulated in brackets [ ]. You can edit the knowledge bases to run your own example-proofs, but you should avoid the use of very long strings in the variable names. Sometimes long variable names create bugs in the display of the proofs, and the program crashes. If such a case occurs, edit the file and replace long strings with shorter ones, as short as possible) Bear in mind that the program does not display bits, but ordinary variables. However, it’s easer this way to understand the workings of the algorithm, tracing variables and  simplifications done using the Three Axioms.

 

My next project is to develop an Assembly Language Version of the “Iphigenia Algorithm”, making use of MMX and SSE extended ASM instructions for the Pentium Processor. This is in fact the closest to “parallelism” we can get, in present-day personal computers.

 

 

11.8) Historical Note, and a… Job Seeking ad:

 

 

 

11.9) Conclusions, Copyright Issues and Acknowledgments

 

 

A simple but extremely efficient algorithm has been outlined, which can reduce a particular class of logic expressions to either a "true" result, or to a "relative minimised result", Such logic expressions (in conventional logic) are of the form "A and B and C.... => a OR b OR c....". This algorithm works by translating such expressions to Multiple Form Logic™, and then applying the Three Axioms of Multiple Form Logic to these expressions, while taking advantage of parallelism and additional simplicity, achieved through a particular kind of encoding into bits (encoding Logic Variables as bit arrays). A demo program was also provided, to make the operation of this algorithm more understandable. This algorithm is highly suited for parallel hardware, e.g. using bit-encoded Laser beams and crystals, storing Logic Knowledge Bases as holograms of bits.

 

It is extremely difficult, today, for an algorithm to be patented. (All legal help and advice on this is appreciated). This algorithm was invented by the author in the year 1986 and was kept a secret till now. I do not preclude the possibility that someone else re-invented this algorithm, during the last seventeen years, but extensive searches and enquiries (made both inside and outside the Internet) showed that no such algorithm was re-invented, since 1986. To safeguard my copyrights, I have posted this algorithm, together with the underlying theory of Multiple Form Logic, inside a stamped addressed envelope mailed to... myself, while living in the UK, in the late eighties. I have never opened it, so it's a “proof of copyright” (under UK law; don't really know if it also guarantees exclusive rights of exploitation of the actual method, stripped of all secrecy, now! ;) )

 

I owe many warm thanks to Dr. Nikos Vainos, research physicist in Lasers (who now works at the National Research Centre, Athens, Greece) for his extremely valuable contributions, as regards a possible implementation of this algorithm in Optical Computing Hardware (even though this hardware was never built, due to lack of funds). He showed me facts about Optical Computing, which led to refinements of the “Iphigenia algorithm”, useful for real implementations: One such refinement is the use of memory copies, rather than a single memory, which can be stored as bit-encoded holograms carved into crystals under different angles; also potentially useful in future implementations of (Prolog-) backtracking. (However, we never built the thing!)

 

I also thank Dr. Tasos Patronis (didactician of Maths for University students, at the University of Patras) for teaching me all he could, in Abstract Algebra and Logic, at the time when the "Theory of Multiple Forms" was being born, for his reference letter (of 1984), and for reading my (sometimes unreadable!) manuscripts, with crucial suggestions for improvements during the early eighties.

 

Finally, I owe a lot to my... mother, the late Iphigenia Stathis (Maths Teacher) for her truly boundless support, while being alive -as all true mothers would! (This algorithm has been named after her, for very real reasons).

Finally, I don't really hate Cretans. They usually... tell the truth!  (And I am not… Cretan, either!)  :-)

 

 

 

The THREE AXIOMS of MULTIPLE FORM LOGIC^™ (for quick hyperlink reference in this document):

 

 

See Also: Extending and improving the bit-crunching Algorithm “Iphigenia”

Next Section: Some Philosophical Aspects of Set Theory and Multiple Form Logic

Previous Section: Proofs of Some Theorems in Multiple Form Logic

Back to the MULTIPLE FORM LOGIC Home Page