Axiom Directed Focusing

DOI10.1007/978-3-642-02444-3_11zbMath1246.03073OpenAlexW1588714103MaRDI QIDQ3638252

Clément Houtmann

Publication date: 2 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00212059v3/file/paper.pdf

zbMATH Keywords

proof theoryfocusingdeduction modulosuperdeduction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theorem proving modulo
• Cut-elimination for a logic with definitions and induction
• Focussing and proof construction
• HOL-λσ: an intentional first-order expression of higher-order logic
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Unbounded Proof-Length Speed-Up in Deduction Modulo
• Superdeduction at Work
• Truth Values Algebras and Proof Normalization
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A Proof-Theoretic Approach to Logic Programming
• Logic Programming with Focusing Proofs in Linear Logic
• Cut Elimination in the Presence of Axioms
• Proof normalization modulo
• Automated Reasoning
• A Simple Proof That Super-Consistency Implies Cut Elimination
• Cut Elimination in Deduction Modulo by Abstract Completion
• Typed Lambda Calculi and Applications