Pages that link to "Item:Q4032862"
From MaRDI portal
The following pages link to Contraction-free sequent calculi for intuitionistic logic (Q4032862):
Displaying 50 items.
- Refined typing to localize the impact of forced strictness on free theorems (Q766167) (← links)
- Graph-based decision for Gödel-Dummett logics (Q877886) (← links)
- The ILTP problem library for intuitionistic logic (Q877897) (← links)
- Inconsistency-tolerant description logic. II: A tableau algorithm for \(\mathcal{CALC}^{\mathsf C}\) (Q946573) (← links)
- Optimization techniques for propositional intuitionistic logic and their implementation (Q959821) (← links)
- Interpolation in non-classical logics (Q1024121) (← links)
- Focusing and polarization in linear, intuitionistic, and classical logics (Q1035706) (← links)
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi (Q1208732) (← links)
- Linearizing intuitionistic implication (Q1210141) (← links)
- Representing scope in intuitionistic deductions (Q1274448) (← links)
- Permutability of proofs in intuitionistic sequent calculi (Q1275625) (← links)
- An improved refutation system for intuitionistic predicate logic (Q1344876) (← links)
- A linear logical framework (Q1400718) (← links)
- Correspondences between classical, intuitionistic and uniform provability (Q1575924) (← links)
- Connection methods in linear logic and proof nets construction (Q1575926) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas (Q1589838) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- From cut-free calculi to automated deduction: the case of bounded contraction (Q1744444) (← links)
- Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem (Q1960430) (← links)
- Sequent calculi for intuitionistic Gödel-Löb logic (Q1982008) (← links)
- Efficient SAT-based proof search in intuitionistic propositional logic (Q2055856) (← links)
- On implicational intermediate logics axiomatizable by formulas minimal in classical logic: a counter-example to the Komori-Kashima problem (Q2062200) (← links)
- SAT-based proof search in intermediate propositional logics (Q2104497) (← links)
- The G4i analogue of a G3i sequent calculus (Q2106879) (← links)
- Loop-check specification for a sequent calculus of temporal logic (Q2106881) (← links)
- Synthesis of modality definitions and a theorem prover for epistemic intuitionistic logic (Q2119125) (← links)
- Terminating calculi and countermodels for constructive modal logics (Q2142091) (← links)
- Proofs and countermodels in non-classical logics (Q2254557) (← links)
- Uniform interpolation and the existence of sequent calculi (Q2326416) (← links)
- Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models (Q2351164) (← links)
- A unified procedure for provability and counter-model generation in minimal implicational logic (Q2397231) (← links)
- Analyticity, balance and non-admissibility of \textit{Cut} in stoic logic (Q2422314) (← links)
- Composition of an intuitionistic negation and negative modalities as a necessity operator (Q2434603) (← links)
- Sufficient conditions for cut elimination with complexity analysis (Q2461191) (← links)
- Decision methods for linearly ordered Heyting algebras (Q2491077) (← links)
- Eigenvariables, bracketing and the decidability of positive minimal predicate logic (Q2503325) (← links)
- Invertible infinitary calculus without loop rules for restricted FTL (Q2577594) (← links)
- GEOMETRISATION OF FIRST-ORDER LOGIC (Q2795295) (← links)
- Contraction-free Proofs and Finitary Games for Linear Logic (Q2805162) (← links)
- An Evaluation-Driven Decision Procedure for G3i (Q2946756) (← links)
- Intuitionistic Decision Procedures Since Gentzen (Q3305556) (← links)
- Labelled Calculi for Łukasiewicz Logics (Q3511458) (← links)
- Deep Inference in Bi-intuitionistic Logic (Q3638293) (← links)
- Intuitionistic Socratic procedures (Q3647238) (← links)
- A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications (Q3647294) (← links)
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme (Q3655207) (← links)
- 1998 European Summer Meeting of the Association for Symbolic Logic (Q4254644) (← links)
- A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs (Q4506460) (← links)
- Generalized tableau systems for intermediate propositional logics (Q4610314) (← links)
