A cut-elimination proof in intuitionistic predicate logic

DOI10.1016/S0168-0072(98)00062-1zbMath0933.03074WikidataQ126989110 ScholiaQ126989110MaRDI QIDQ1304543

Mirjana Borisavljević

Publication date: 20 March 2000

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

cut eliminationsequent calculuslinear logiccut rulestructural rulescontraction rulereduction tree of a derivationweighted rank

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (3)

A connection between cut elimination and normalization ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Computing interpolants in implicational logics

Cites Work

• Algebra of proofs
• The correspondence between cut-elimination and normalization

This page was built for publication: A cut-elimination proof in intuitionistic predicate logic