(Dual) Hoops Have Unique Halving
This work addresses foundational issues in the model theory of continuous structures for logicians, but it is incremental as it builds on existing algebraic frameworks.
The paper tackled the problem of proving an important algebraic law in propositional continuous logic, which extends multi-valued Lukasiewicz logic with a halving operator, and they successfully proved that dual hoops have unique halving using automated theorem proving.
Continuous logic extends the multi-valued Lukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The semantics of these logics can be given using specialisations of algebraic structures known as hoops. As part of an investigation into the metatheory of propositional continuous logic, we were indebted to Prover9 for finding a proof of an important algebraic law.