A new algorithm for derivability in the constructive propositional calculus
From MaRDI portal
Publication:5608767
DOI10.1090/TRANS2/094/02zbMATH Open0208.01905OpenAlexW4214599228MaRDI QIDQ5608767FDOQ5608767
Authors: Nikolai Nikolaevic Vorob'Ev
Publication date: 1970
Published in: Sixteen Papers on Logic and Algebra (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1090/trans2/094/02
Cited In (14)
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- The G4i analogue of a G3i sequent calculus
- Invertible infinitary calculus without loop rules for restricted FTL
- Terminating calculi for propositional Dummett logic with subformula property
- An intuitionistic formula hierarchy based on high‐school identities
- Linear depth deduction with subformula property for intuitionistic epistemic logic
- Uniform interpolation and the existence of sequent calculi
- Intuitionistic Decision Procedures Since Gentzen
- Proof theory for Lax Logic
- Admissibility of structural rules for contraction-free systems of intuitionistic logic
- Proof-theoretical investigation of temporal logic with time gaps
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
- A unified procedure for provability and counter-model generation in minimal implicational logic
- Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
This page was built for publication: A new algorithm for derivability in the constructive propositional calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5608767)