[FOM] Truth value algorithm for tokens
Axiomize@aol.com
Axiomize at aol.com
Mon Nov 4 15:08:51 EST 2002
On 30 Oct 2002, Sandy Hodges wrote:
> I've posted a write-up of my latest algorithm. As always,
> comments and refutations are appreciated.
> Token a: ~ Fa(d) & (0=0 <=> Fa(c)) false
> Token b: ~ ((Tr(c) => Tr(d)) or Fa(a)) gap
> Token c: (Tr(g) or 1=0) & Fa(d) <=> (~ Tr(f) <=> 1=0) gap
> Token d: 0=0 <=> Tr(d) or Tr(a) gap
> Token e: 1=0 & Tr(c) <=> (Tr(e) <=> Fa(g)) gap
> Token f: ~ ((0=0 <=> Tr(c)) or (Fa(b) <=> Tr(c))) gap
> Token g: ~ Fa(h) & (Fa(d) => Fa(e)) true
> Token h: ~ (Tr(b) & (Fa(a) or Tr(g))) true
Is this not the satisfiability (SAT) problem? That is, each token is a
Boolean variable, each such variable x that states a formula y means that x<=>
y, creating xv~y and ~xvy, and if the resulting clauses are not satisfiable
then we have a paradox.
"This is false." yields clauses x and ~x, while "This is true." yields clause
xv~x.
If gap is allowed as a value, then we have the multivalued satisfiablility
problem. In this case, each 3-valued variable can be encoded into 2 Boolean
variables, or 3 Boolean variables where each original value (true, false,
gap) is represented by a separate Boolean variable ("one-hot encoding").
One-hot encoded, let Boolean variables a1, a2 and a3 represent Token a being
true, false and gap, respectively, and similarly for Tokens b-h. Then the
clauses by definition of the variables for Token a are:
a1 v a2 v a3
~a1 v ~a2
~a1 v ~a3
~a2 v ~a3
Token a states a1<=>(~d2^c2) creating a1v~(~d2^c2) and ~a1v(~d2^c2) for
clauses:
a1 v d2 v ~c2
~a1 v ~d2
~a1 v c2
and similarly for the other tokens.
Would it be better to use established terminology and relate your methods to
the vast literature on the SAT problem (e.g. the Davis-Putnam algorithm and
its derivatives)?
Charlie Volkstorf
Cambridge, MA
> Sandy Hodges / Alameda, California, USA
> mail to SandyHodges at attbi.com will reach me.
More information about the FOM
mailing list