Evaluation Trees for Proposition Algebra

Abstract

Proposition algebra is based on Hoare’s conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so-called free valuation congruence: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Free valuation congruence is axiomatized by the four basic equational axioms of proposition algebra that define the conditional connective. A valuation congruence that is axiomatized in proposition algebra and that identifies more conditional statements than free valuation congruence is repetition-proof valuation congruence, which we characterize by a simple transformation on evaluation trees.

Dedicated to Ernst-Rüdiger Olderog on the occasion of his sixtieth birthday. Jan Bergstra recalls many discussions during various meetings as well as joint work with Ernst-Rüdiger and Jan Willem Klop on readies, failures, and chaos back in 1987. Alban Ponse has pleasant memories of the process of publishing [8], the Selected Papers from the Workshop on Assertional Methods, of which Ernst-Rüdiger, who was one of the invited speakers at this workshop (held at CWI in November 1992), is one of the guest editors. An extended version of this paper appeared as report [6].