zbMATH — the first resource for mathematics

Dual intuitionistic logic revisited. (English) Zbl 0963.03042
Dyckhoff, Roy (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2000, St Andrews, Scotland, GB, July 3-7, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1847, 252-267 (2000).
Summary: We unify the algebraic, relational and sequent methods used by various authors to investigate “dual intuitionistic logic”. We show that restrictirig sequents to “singletons on the left/right” cannot capture “intuitionistic logic with dual operators”, the natural hybrid logic that arises from intuitionistic and dual-intuitionistic logic. We show that a previously reported generalised display framework does deliver the required cut-free display calculus. We also pinpoint precisely the structural rule necessary to turn this display calculus into one for classical logic.
For the entire collection see [Zbl 0941.00032].

03B55 Intermediate logics
03F05 Cut-elimination and normal-form theorems
03B35 Mechanization of proofs and logical operations