Prove that algebraic structure is not semiring?

2011-11-28T21:50:28Z

I have a [finite] lattice enriched with additional operations. I would like either:

find a pair of binary operations (and constants) satisfying semiring laws, or
prove that no such operations exist

As the structure is finite, one can approach problem #1 via computerized search. For illustration purpose if I had boolean algebra with operations $\vee$, $\wedge$, and $\neg$, then the search would return semiring operations $\oplus$ and $\otimes$ expressed via those. However, if this search fails, how would I prove that no such operations exist?

I assume that there are fundamental properties of semirings, that can be employed. By "fundamental" I mean that they don't explicitly refer to semiring operations; they only assume that such operations exist. Therefore, one just have to show that my lattice doesn't possess those. So what are fundamental properties of semirings?

Edit: to give a justification why I suspect semiring structure can exist is that my lattice is in many respects is similar to relation algebra. Unfortunately, what might be considered the intuitive analogous of composition operation is not associative. Yet, the structure contains more than one instance of everything: there are two conjunction, two disjunctions, two negations, and four constants, so there might be more than one way to manufacture composition.

Answer by Jacques Carette for Prove that algebraic structure is not semiring?

2011-11-29T00:19:31Z

I will interpret your question to mean:

Is there a small (closed-form) expression in the existing symbols in my algebraic structure which can be interpreted as $\oplus$ and $\otimes$ for a semiring?

Of course, this also assumes you have candidates for $0$ and $1$. I would use the finite model verifier Mace4 for this. If you want to see a nice example of this technique in action, I recommend Modal semirings revisited by Desharnais and Struth. They use both Prover9 and Mace4 for finding structures and disproving that some exist, in a very similar domain to yours. P.14 of that paper even shows some sample input for those programs to get the kinds of results you want. Another place to look is this repository of Prover9 files.

Prove that algebraic structure is not semiring? - MathOverflow

Prove that algebraic structure is not semiring?

Answer by Jacques Carette for Prove that algebraic structure is not semiring?