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 (10)

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

This page was built for publication: Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic