Subformula Linking as an Interaction Method

DOI10.1007/978-3-642-39634-2_28MaRDI QIDQ5327358zbMATH OpenOpenAlexFDO

Authors Kaustuv Chaudhuri

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00937009/file/formula_linking.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Recommendations

• Submodel-defining formulas
• scientific article; zbMATH DE number 1487957
• Linking forms revisited
• scientific article; zbMATH DE number 4102101
• scientific article; zbMATH DE number 4044772
• Subtyping in logical form
• An application of substructure method
• scientific article; zbMATH DE number 166707

Cited in

(3)

• Subformula linking for intuitionistic logic with application to type theory
• On the Power of Substitution in the Calculus of Structures
• The flower calculus

This page was built for publication: Subformula Linking as an Interaction Method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327358)