17) Extending and improving the bit-crunching Algorithm “Iphigenia”
Algorithm “Iphigenia” was invented in 1987 and implemented as a demo program (“bitprover”) in 1990. Soon afterwards, it became evident that the dream of creating optical computing hardware using this algorithm (in cooperation with Dr. Nikos Vainos) had to be postponed indefinitely due to lack of funds. So, all further work on this algorithm was suspended, while I became involved in other types of work (article writing and software dictionary development). However, in recent work reviving this algorithm, it became evident that the range of logic expressions, which can be stored as “bit-patterns for logic deduction”, can be extended in a number of ways. For example:
Expressions of the form “(A
and B and C and…) => (a and b and…)”: These can be converted to multiple (AND-ed)
expressions of the form:
“(
(A and B and C and…) => a) and ((A and B and C and…) => b) and… “.
In Multiple Form Logic this can be massaged by distributivity (e.g. theorem T5), as follows:
A
and B and C… ) => (a and b and…)))#1 becomes:
(A#1,B#1,C#1,
(a#1,b#1,..)#1)#1 which becomes:
(A#1,B#1,C#1,a)#1,
(A#1,B#1,C#1,b)#1, … (of the same form as the original logic
expressions allowable in the algorithm’s bit-encoded knowledge base,
i.e. “(X
and Y and Y) => a or b or… “).
Expressions of the form “(A=B)
and (C=D) and… ) => etc.” (with logic equalities such as X=Y)
can be converted by turning each equality X=Y
into a composite expression ((X#1,Y)#1,(X,Y#1)#1)#1
and then treating each term as a separate expression (AND-ed
with the rest).
E.g. To prove an implication in Equational
Boolean Logic: ((A=B)
and (B=C)) => (A=C), first we translate the premises “((A=B)
and (B=C))” into:
(A#1,B)#1,
(A,B#1)#1, (B#1,C)#1 , (C#1,B)#1, i.e. (in bit array format):
100
010 (A#1,B)#1
010
100 (A,B#1)#1
010
001 (B#1,C)#1
001
010 (B,C#1)#1
And then we can apply two independent
logic queries: A=>C
and C=>A,
to evaluate “A=C”:
100 010 (A#1,B)#1 -“vertical
cancellation rule” RVC
010
100 (A,B#1)#1
010
001 (B#1,C)#1 -“vertical
cancellation rule” RVC
001
010 (B,C#1)#1
100 001 (A#1,C) -logic query
(1): “A=>C
” ?
100
010 (A#1,B)#1
010
100 (A,B#1)#1 -“vertical
cancellation rule” RVC
010
001 (B#1,C)#1
001 010 (B,C#1)#1 -“vertical
cancellation rule” RVC
001 100 (A#1,C) -logic query
(2): “C=>A” ?
(using
two independent copies of the bit-array knowledge base). The
results are easy to get:
000
010 (A#1,B)#1
-isolated bit - row
010
100 (A,B#1)#1
010
000 (B#1,C)#1
001 010 (B,C#1)#1
100
001 (A#1,C) -logic query (1): “A=>C
”
?
100
010 (A#1,B)#1
010
000 (A,B#1)#1
010
001 (B#1,C)#1
000
010 (B,C#1)#1
-isolated bit - row
001
100 (A#1,C) -logic query (2): “C=>A”
?
The “next generations” (after “transferring isolated bits diagonally” by rule “RDT”) are:
010
100 (A,B#1)#1
010
000 (B#1,C)#1
-“zeroed row” (i.e. result = “TRUE”)
001
010 (B,C#1)#1
110
001 (A#1,C) -a
new bit
transferred diagonally
100
010 (A#1,B)#1
010
000 (A,B#1)#1 -“zeroed row” (i.e. result =
“TRUE”)
010
001 (B#1,C)#1
011
100 (A#1,C) -a
new bit
transferred diagonally
So it was straightforward to answer the query “A=C”, proving it true (given “A=B and B=C”).
The
range of logic expressions
which can be converted to Iphigenia-compatible
bit-encoded arrays
can of course be extended further. Readers familiar with
PROLOG and
Horn Clause Logic
may have realised that each “bit-encoded row”, in such a
logic system, resembles a Prolog Clause
of the form
Goal
<= A and B and C...” -
except that (at this stage) such
expressions do not contain variables.
Now, since (almost) any logic expression can be translated to
Horn-Clauses, it can also
be translated into “bit-array
patterns” for bit-crunching
algorithm “Iphigenia”.
The only real problem is how to deal with variables and predicate logic expressions, rather than propositional logic expressions.
Well, here are some crucial steps, on the road to arriving there:
Next section:
Elementary
Variables and Unifications
in Multiple
Form Logic™