Quasi-boolean equivalence (Q2366071)

Many program derivations are simplified if one allows the occurrence of certain Boolean subexpressions to which no value can reasonably be attributed. For instance, \(x\vee y\) ought to have the value true if \(x\) does, even if \(y\) is undefined. Such expressions are traditionally handled by the conditional connectives cand and cor, but these do not satisfy pleasant algebraic laws. The paper shows that it is safe to apply the rules for constructing equational proofs in the style of Dijkstra [\textit{E. W. Dijkstra} and \textit{C. S. Scholton}, Predicate calculus and program semantics, New York: Springer (1990; Zbl 0698.68011)] as if all subexpressions were well- defined. That is, possible undefinedness of subexpressions may be ignored.