Focused Inductive Theorem Proving

DOI10.1007/978-3-642-14203-1_24zbMath1291.68322OpenAlexW1507932752MaRDI QIDQ5747767

Zachary Snow, David Baelde, Dale A. Miller

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_24

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

Cut elimination for a logic with induction and co-induction ⋮ A Proposal for Broad Spectrum Proof Certificates

Uses Software

• Tac

Cites Work

• Unnamed Item
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Cut-elimination for a logic with definitions and induction
• On the Expressivity of Minimal Generic Quantification
• Focusing and Polarization in Intuitionistic Logic
• Logic Programming with Focusing Proofs in Linear Logic
• Computer Science Logic
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Types for Proofs and Programs
• Least and Greatest Fixed Points in Linear Logic

This page was built for publication: Focused Inductive Theorem Proving