scientific article

zbMath1036.03003MaRDI QIDQ2703802

Grigori Mints

Publication date: 18 March 2001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

sequent calculusnormalizationnatural deductioninterpolation theoremintuitionistic logicKripke modelcut-eliminationdisjunction propertytableaux systemCurry-Howard isomorphismGlivenko's theoremBHK-interpretation

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (32)

An Arithmetical Interpretation of Verification and Intuitionistic Knowledge ⋮ The Gödel-Tarski Translations of Intuitionistic Propositional Formulas ⋮ Abstract Hilbertian deductive systems, infon logic, and Datalog ⋮ COMPLETE INTUITIONISTIC TEMPORAL LOGICS FOR TOPOLOGICAL DYNAMICS ⋮ Exploring the Jungle of Intuitionistic Temporal Logics ⋮ Strong Equivalence and Program Structure in Arguing Essential Equivalence between Logic Programs ⋮ Proving infinitary formulas ⋮ Wansing's bi-intuitionistic logic: semantics, extension and unilateralisation ⋮ Negational fragment of intuitionistic control logic ⋮ Conservative translations revisited ⋮ Completeness of \(\mathrm S4\) for the Lebesgue measure algebra ⋮ On intuitionistic modal and tense logics and their classical companion logics: topological semantics and bisimulations ⋮ Hypersequent calculi for intuitionistic logic with classical atoms ⋮ An \(\mathsf{AC}^{1}\)-complete model checking problem for intuitionistic logic ⋮ Some topological properties of paraconsistent models ⋮ Minimal change: relevance and recovery revisited ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Basic Constructive Connectives, Determinism and Matrix-Based Semantics ⋮ 2002–2003 Winter Meeting of the Association for Symbolic Logic ⋮ On expressive power of basic modal intuitionistic logic as a fragment of classical FOL ⋮ Second-order abstract categorial grammars as hyperedge replacement grammars ⋮ DKAL and Z3: A Logic Embedding Experiment ⋮ A proof of topological completeness for S4 in \((0,1)\) ⋮ Computing interpolants in implicational logics ⋮ Kripke semantics for fuzzy logics ⋮ HasCasl: integrated higher-order specification and program development ⋮ Intuitionistic Existential Instantiation and Epsilon Symbol ⋮ Automating Theories in Intuitionistic Logic ⋮ A polynomial translation of S4 into intuitionistic logic ⋮ Topological Semantics for da Costa Paraconsistent Logics $$C_\omega $$ C ω and $$C^{*}_\omega $$ C ω ∗ ⋮ Failure of Interpolation in Constant Domain Intuitionistic Logic ⋮ Cut elimination for S4C: A case study

This page was built for publication: