[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:

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]