Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic

DOI10.1093/logcom/exn067zbMath1189.03070OpenAlexW2160399032MaRDI QIDQ3406690

Rajeev Goré, Linda Postniece

Publication date: 19 February 2010

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.613.4518

zbMATH Keywords

sequent calculussubtractive logicproof searchdecision procedurebi-intuitionistic logicHeyting-Brouwer logicrefutation calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Bi-simulating in bi-intuitionistic logic, Bi-intuitionistic implication structures, The semi Heyting-Brouwer logic, Kripke Semantics for Basic Sequent Systems, Proofs and countermodels in non-classical logics, A MODAL TRANSLATION FOR DUAL-INTUITIONISTIC LOGIC, Deep Inference in Bi-intuitionistic Logic, A connection-based characterization of bi-intuitionistic validity, Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models, Structuring co-constructive logic for proofs and refutations