A new algorithm for derivability in the constructive propositional calculus

DOI10.1090/TRANS2/094/02MaRDI QIDQ5608767zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Other constructive mathematics (03F65)

Cited in

(14)

• Intuitionistic Decision Procedures Since Gentzen
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• Proof theory for Lax Logic
• Invertible infinitary calculus without loop rules for restricted FTL
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• An intuitionistic formula hierarchy based on high‐school identities
• Proof-theoretical investigation of temporal logic with time gaps
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Linear depth deduction with subformula property for intuitionistic epistemic logic
• A unified procedure for provability and counter-model generation in minimal implicational logic
• Uniform interpolation and the existence of sequent calculi
• The G4i analogue of a G3i sequent calculus
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Terminating calculi for propositional Dummett logic with subformula property

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)