Dual Tableaux for Logics of Conditional Decisions

Abstract

The roots of the logics and algebras of conditional decisions can be traced back to the work by Claude Elwood Shanon in [Sha38] and his information theory [Sha48].

Logics of conditional decisions are the formalisms for the specification of n≥ 2 alternative decisions that depend on a condition which holds in a degree. In the binary case the formulas of the logic may be viewed as binary decision trees or if-then-elsestatements which represent branching in algorithms; they are the basic statements in most of the programming languages. The paper [McC63] is one of the foundations of that research. Binary decision diagrams were introduced in [Lee59] as a compact representation of binary decision trees used for a representation of Boolean functions; see also [Ake78]. They are extensively applied to the synthesis of combinatorial circuits and in the implementation and formal verification of systems. Interest in multiple-valued branching was inspired by observations in [Dij68].