×

How to augment a formal system with a Boolean algebra component. (English) Zbl 0967.03011

Bibel, Wolfgang (ed.) et al., Automated deduction. A basis for applications. Vol. III: Applications. Dordrecht: Kluwer Academic Publishers; 0-7923-5132-0 (set)). Appl. Log. Ser. 10, 57-75 (1998).
From the introduction: Reasoning with Boolean algebras is just propositional reasoning. This is well investigated and a lot of good algorithms have been developed. Other formal systems, for example mathematical programming for reasoning about arithmetical equation systems, are equally well developed. Combining such a system with a Boolean component where the Boolean expressions are interpreted as sets, would allow one to use arithmetical algorithms to reason about numerical features of sets.
In this chapter we introduce the atomic decomposition technique as a means to combine computation and reasoning in a given formal system with reasoning about Boolean algebras and features of the elements of the Boolean algebra which make sense in the given basic system. Propositional reasoning is invoked in a kind of compilation phase which eliminates the Boolean algebra part of the problem completely and shifts the main reasoning problem to the basic system. The decomposition method works for combinations of formal systems with a Boolean algebra component, where the Boolean terms are embedded in bridging functions mapping the Boolean parts to objects the given formal system can understand.
For the entire collection see [Zbl 0954.00010].

MSC:

03B35 Mechanization of proofs and logical operations
03G05 Logical aspects of Boolean algebras
PDFBibTeX XMLCite