Distributivity Laws in Residuated Binars with Involution

To reproduce the results presented during AITP 2021, follow installation instructions, then naviage to examples/reproducing-papers.ipynb.

If you would like to learn more about this work, see 6th Conference on Artificial Intelligence and Theorem Proving

For previous work in this field and more mathematical context see Fussner, W., Jipsen, P. Distributive laws in residuated binars. Algebra Univers. 80, 54 (2019).

Additional Files Descriptions

DistributiveCase.thy

A human-written proof of one of the known statements about distributivity in residuated binars.

notebooks/binars.pkl

A serialisation of tabular representation of six binars serving as a proof of the distributivity law independence mentioned in the paper.

notebooks/rb-check.ipynb

This file is a contribution of Carlos Simpson. It checks algebraic properties of binars.pkl

notebooks/another-check.ipynb

Another file for checking algebraic properties of binars.pkl