Adas and the equational theory of if-then-else (Q690107)

The paper studies the equational theory of the ternary if-then-else operation. It gives results on the classical two-valaued and the programming-language-oriented three-valued interpretations. It adds to the previous literature a completeness theorem relating the underlying axiom systems. In the three-valued case, it also ties in the sequential connectives (also known as conditional and/or). Besides its value within universal algebra it therefore is also useful in programming theory. The equational laws of if-then-else are almost daily used subconsciously in programming practice. So the paper would also be interesting to ``everyday'' programmers, although they will find it a bit hard to digest.