Generalized MV Algebras (GMV)

Tomasz Kowalski, Francesco Paoli and Robert Veroff

February 2010

This page presents syntactic proofs for a problem (described here) in Generalized MV algebras. The proofs were found with the assistance of the program Prover9 [1].

Axioms

(x ^ y) ^ z = x ^ (y ^ z)               # label("Associativity-^").   
(x V y) V z = x V (y V z)               # label("Associativity-V").
x ^ x = x                               # label("Idempotence-^").
x V x = x                               # label("Idempotence-V").
x ^ y = y ^ x                           # label("Commutativity-^").
x V y = y V x                           # label("Commutativity-V").
(x ^ y) V x = x                         # label("Absorption a").
(x V y) ^ x = x                         # label("Absorption b").

(x * ((x \ z) ^ y)) V z = z             # label("Residual a").
((y ^ (z / x)) * x) V z = z             # label("Residual b").
(x \ ((x * y) V z)) ^ y = y             # label("Residual c").
(((y * x) V z) / x) ^ y = y             # label("Residual d").

(x * y) * z = x * (y * z)               # label("Associativity-* (fusion)").
1 * x = x                               # label("Left monoid unit").
x * 1 = x                               # label("Right monoid unit").

x V y = x / ((x V y) \ x)               # label("GMV a").
x V y = (x / (x V y)) \ x               # label("GMV b").

x @ y = (x * (x \ 1)) * ((y \ 1) \ 1)   # label("Definition-@").

Goals

x @ x = x                               # label("Goal 1").
(x @ y) @ z = x @ z                     # label("Goal 2").
x @ (y @ z) = x @ z                     # label("Goal 3").
  
(x ^ y) @ (z ^ u) = (x @ z) ^ (y @ u)   # label("Goal 4").
(x V y) @ (z V u) = (x @ z) V (y @ u)   # label("Goal 5").
(x \ y) @ (z \ u) = (x @ z) \ (y @ u)   # label("Goal 6").
(x / y) @ (z / u) = (x @ z) / (y @ u)   # label("Goal 7").
  
(x * (x \ 1)) @ 1 = x * (x \ 1)         # label("Goal 8").
1 @ (x * (x \ 1)) = 1                   # label("Goal 9").
(x \ 1) @ 1 = 1                         # label("Goal 10").
1 @ (x \ 1) = x \ 1                     # label("Goal 11").
  
(x / (y \ x)) @ (x V y) = x V y         # label("Goal 12").
((x / y) \ x) @ (x V y) = x V y         # label("Goal 13").
(x V y) @ (x / (y \ x)) = x / (y \ x)   # label("Goal 14").
(x V y) @ ((x / y) \ x) = (x / y) \ x   # label("Goal 15").

Proofs

We include input, output, proof and xml files created as follows.

prover9 -f file.in > file.out prooftrans -f file.out > file.pf
prooftrans xml -f file.out > file.xml

These essentially are proof-checking runs, since they include steps from previously found proofs as hints. The original proofs were found using the method of proof sketches [2]. In particular, our approach was to find derivations with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired proofs.

Prove all 15 goals in a single Prover9 run
Proof. (in, out, pf, xml)
These 15 proofs are strictly forward and demodulation free (SFDF). That is, they are derivations of the goals from the axioms (strictly forward), and the proof steps are single applications of an inference rule, without rewriting (demodulation free).

References

W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
R. Veroff. Solving Open Questions and Other Challenge Problems Using Proof Sketches. Journal of Automated Reasoning, 27(2):157-174, 2001. (postscript)