[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

## Problem #82

Originator: J. Zhang
Date: April 1995

Summary: Is there a convergent extended rewrite system for ternary boolean algebra, in which certain equations hold?

Is there a convergent extended rewrite system for ternary boolean algebra, for which the following permutative equations hold:

 f(x, y, z) = f(x, z, y) = f(y, x, z) = f(y, z, x) = f(z, x, y) = f(z, y, x) f(f(x, y, z), u, x) = f(x, y, f(z, u, x))

See [Wos][Zhaar][Chr][Fri85].

### Comment sent by Hansjörg Lehner

Date: Wed Dec 20 17:46:07 MET 2000

```The following permutative equations hold for every ternary boolean algebra:

f(f(x, y, z), u, x) = f(x, y, f(z, u, x))
f(x, y, z) = f(x, z, y) = f(y, x, z) = f(y, z, x) = f(z, x, y) = f(z, y, x)

Consider the following set of axioms:

Axiom 1: f(f(x1,x2,x3),x4,f(x1,x2,x5)) = f(x1,x2,f(x3,x4,x5))
Axiom 2: f(x1,x1,x2) = x1

This theorem holds true:

Theorem 1: f(f(A,B,C),D,A) = f(A,B,f(C,D,A))

Proof:

Lemma 1: z = f(z,x4,z)

z
=    by Axiom 2 RL
f(z,z,f(y,x4,x5))
=    by Axiom 1 RL
f(f(z,z,y),x4,f(z,z,x5))
=    by Axiom 2 LR
f(z,x4,f(z,z,x5))
=    by Axiom 2 LR
f(z,x4,z)

Theorem 1: f(f(A,B,C),D,A) = f(A,B,f(C,D,A))

f(f(A,B,C),D,A)
=    by Lemma 1 LR
f(f(A,B,C),D,f(A,B,A))
=    by Axiom 1 LR
f(A,B,f(C,D,A))

Consider the following set of axioms:

Axiom 1: x1 = f(x2,x1,x1)
Axiom 2: x1 = f(x1,x2,g(x2))
Axiom 3: f(x1,x2,f(x3,x4,x5)) = f(f(x1,x2,x3),x4,f(x1,x2,x5))

This theorem holds true:

Theorem 1: f(A,B,C) = f(B,A,C)

Proof:

Lemma 1: f(f(g(x1),x0,q),x0,x1) = f(g(x1),x0,x1)

f(f(g(x1),x0,q),x0,x1)
=    by Axiom 2 LR
f(f(f(g(x1),x0,q),x1,g(x1)),x0,x1)
=    by Axiom 1 LR
f(f(f(g(x1),x0,q),x1,g(x1)),x0,f(f(g(x1),x0,q),x1,x1))
=    by Axiom 3 RL
f(f(g(x1),x0,q),x1,f(g(x1),x0,x1))
=    by Axiom 3 RL
f(g(x1),x0,f(q,x1,x1))
=    by Axiom 1 RL
f(g(x1),x0,x1)

Lemma 2: f(g(g(y)),y,q) = g(g(y))

f(g(g(y)),y,q)
=    by Axiom 2 LR
f(f(g(g(y)),y,q),y,g(y))
=    by Lemma 1 LR
f(g(g(y)),y,g(y))
=    by Axiom 2 RL
g(g(y))

Lemma 3: g(g(z)) = z

g(g(z))
=    by Lemma 2 RL
f(g(g(z)),z,z)
=    by Axiom 1 RL
z

Lemma 4: f(y,y,q) = y

f(y,y,q)
=    by Lemma 3 RL
f(g(g(y)),y,q)
=    by Lemma 2 LR
g(g(y))
=    by Lemma 3 LR
y

Lemma 5: f(g(x1),y,x1) = y

f(g(x1),y,x1)
=    by Lemma 1 RL
f(f(g(x1),y,y),y,x1)
=    by Axiom 1 RL
f(y,y,x1)
=    by Lemma 4 LR
y

Lemma 6: f(v,u,x4) = f(u,x4,v)

f(v,u,x4)
=    by Lemma 5 RL
f(v,u,f(g(v),x4,v))
=    by Axiom 3 LR
f(f(v,u,g(v)),x4,f(v,u,v))
=    by Axiom 1 LR
f(f(v,u,g(v)),x4,f(f(v,v,v),u,v))
=    by Axiom 1 LR
f(f(v,u,g(v)),x4,f(f(v,v,v),u,f(v,v,v)))
=    by Axiom 3 RL
f(f(v,u,g(v)),x4,f(v,v,f(v,u,v)))
=    by Lemma 4 LR
f(f(v,u,g(v)),x4,v)
=    by Lemma 3 RL
f(f(g(g(v)),u,g(v)),x4,v)
=    by Lemma 5 LR
f(u,x4,v)

Theorem 1: f(A,B,C) = f(B,A,C)

f(A,B,C)
=    by Lemma 6 RL
f(C,A,B)
=    by Lemma 5 RL
f(C,A,f(g(A),B,A))
=    by Axiom 3 LR
f(f(C,A,g(A)),B,f(C,A,A))
=    by Axiom 1 RL
f(f(C,A,g(A)),B,A)
=    by Axiom 2 RL
f(C,B,A)
=    by Lemma 6 LR
f(B,A,C)

Consider the following set of axioms:

Axiom 1: x1 = f(x2,x1,x1)
Axiom 2: x1 = f(x1,x2,g(x2))
Axiom 3: f(x1,x2,f(x3,x4,x5)) = f(f(x1,x2,x3),x4,f(x1,x2,x5))

This theorem holds true:

Theorem 1: f(A,B,C) = f(A,C,B)

Proof:

Lemma 1: f(v,u,f(g(u),x4,u)) = f(v,x4,u)

f(v,u,f(g(u),x4,u))
=    by Axiom 3 LR
f(f(v,u,g(u)),x4,f(v,u,u))
=    by Axiom 1 RL
f(f(v,u,g(u)),x4,u)
=    by Axiom 2 RL
f(v,x4,u)

Lemma 2: f(f(g(x1),x0,q),x0,x1) = f(g(x1),x0,x1)

f(f(g(x1),x0,q),x0,x1)
=    by Lemma 1 RL
f(f(g(x1),x0,q),x1,f(g(x1),x0,x1))
=    by Axiom 3 RL
f(g(x1),x0,f(q,x1,x1))
=    by Axiom 1 RL
f(g(x1),x0,x1)

Lemma 3: f(g(g(y)),y,q) = g(g(y))

f(g(g(y)),y,q)
=    by Axiom 2 LR
f(f(g(g(y)),y,q),y,g(y))
=    by Lemma 2 LR
f(g(g(y)),y,g(y))
=    by Axiom 2 RL
g(g(y))

Lemma 4: g(g(z)) = z

g(g(z))
=    by Lemma 3 RL
f(g(g(z)),z,z)
=    by Axiom 1 RL
z

Lemma 5: f(y,y,q) = y

f(y,y,q)
=    by Lemma 4 RL
f(g(g(y)),y,q)
=    by Lemma 3 LR
g(g(y))
=    by Lemma 4 LR
y

Lemma 6: f(v,u,x4) = f(v,x4,u)

f(v,u,x4)
=    by Lemma 5 RL
f(v,u,f(x4,x4,u))
=    by Axiom 1 LR
f(v,u,f(f(g(u),x4,x4),x4,u))
=    by Lemma 2 LR
f(v,u,f(g(u),x4,u))
=    by Lemma 1 LR
f(v,x4,u)

Theorem 1: f(A,B,C) = f(A,C,B)

f(A,B,C)
=    by Lemma 6 LR
f(A,C,B)
```

## References

[Chr]
Jim Christian. Problem corner: An experiment with Grau’s ternary Boolean algebra. Submitted.
[Fri85]
Laurent Fribourg. A superposition oriented theorem prover. Theoretical Computer Science, 35:161, 1985.
[Wos]
Larry Wos. Automated reasoning: 33 basic research problems.
[Zhaar]
J. Zhang. A 3-place commutative operator from TBA. AAR Newsletters, to appear.

 [Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]