Prove that algebraic structure is not semiring? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T11:31:39Z http://mathoverflow.net/feeds/question/82117 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/82117/prove-that-algebraic-structure-is-not-semiring Prove that algebraic structure is not semiring? Tegiri Nenashi 2011-11-28T21:50:28Z 2011-11-29T00:19:31Z <p>I have a [finite] lattice enriched with additional operations. I would like either: </p> <ol> <li>find a pair of binary operations (and constants) satisfying semiring laws, or</li> <li>prove that no such operations exist</li> </ol> <p>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?</p> <p>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? </p> <p><em>Edit:</em> 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. </p> http://mathoverflow.net/questions/82117/prove-that-algebraic-structure-is-not-semiring/82129#82129 Answer by Jacques Carette for Prove that algebraic structure is not semiring? Jacques Carette 2011-11-29T00:19:31Z 2011-11-29T00:19:31Z <p>I will interpret your question to mean:</p> <blockquote> <p>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?</p> </blockquote> <p>Of course, this also assumes you have candidates for $0$ and $1$. I would use the <a href="http://www.cs.unm.edu/~mccune/mace4/" rel="nofollow">finite model verifier Mace4</a> for this. If you want to see a nice example of this technique in action, I recommend <a href="http://www.dcs.shef.ac.uk/intranet/research/resmes/CS0801.pdf" rel="nofollow">Modal semirings revisited</a> 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 <a href="http://staffwww.dcs.shef.ac.uk/people/G.Struth/ka/" rel="nofollow">this repository</a> of Prover9 files.</p>