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].
(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-@").
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").
prover9 -f file.in > file.outThese 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.prooftrans -f file.out > file.pf
prooftrans xml -f file.out > file.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).