Subformula linking for intuitionistic logic with application to type theory

DOI10.1007/978-3-030-79876-5_12OpenAlexW3178958520MaRDI QIDQ2055855

Kaustuv Chaudhuri

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_12

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• MELL in the calculus of structures
• A two-level logic approach to reasoning about computations
• Logic Programming with Focusing Proofs in Linear Logic
• A framework for defining logics
• Abella: A System for Reasoning about Relational Specifications
• Subformula Linking as an Interaction Method
• A Local System for Intuitionistic Logic
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item