Dual Tableaux for Threshold Logics

Abstract

Threshold logics are a tool for specification, design, and verification of switching circuits constructed from electronic gates. One of the first ideas in this direction can be found in [PM60]; see also [Der65]. Threshold logics developed as a circuit design paradigm alternative to the classical Boolean logic. A threshold element is a generalization of a conventional gate. A single threshold element can represent a number of switching functions obtained through various combinations of weights and a threshold. The concept of threshold provides a representation of a level and switching states below or above the level. A survey of the development and applications of threshold logics can be found in [BQA03, Mur71].

In this chapter we consider a class of first-order threshold logics such that the weights and the thresholds are elements of a commutative group. We develop dual tableaux for this class of logics and we prove their completeness. Next, we show that the standard threshold logic based on the additive group of integers is mutually interpretable with the classical first-order logic. In the above mentioned applications the propositional calculus of this standard threshold logic is used. The dual tableaux presented in this chapter originated in [Orł74, Orł76]. Their generalization to threshold logics based on arbitrary groups was developed in [Cie80].