Axiom Directed Focusing

DOI10.1007/978-3-642-02444-3_11MaRDI QIDQ3638252zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Superdeduction at Work
• Superdeduction in \(\bar{\lambda}\mu\tilde{\mu}\)
• A Simple Proof That Super-Consistency Implies Cut Elimination
• A simple proof that super-consistency implies cut elimination
• Cut Elimination in Deduction Modulo by Abstract Completion

Cites work

• scientific article; zbMATH DE number 1082077 (Why is no real title available?)
• scientific article; zbMATH DE number 3074068 (Why is no real title available?)
• A Proof-Theoretic Approach to Logic Programming
• A Simple Proof That Super-Consistency Implies Cut Elimination
• Automated Reasoning
• Cut Elimination in Deduction Modulo by Abstract Completion
• Cut Elimination in the Presence of Axioms
• Cut-elimination for a logic with definitions and induction
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Focussing and proof construction
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
• Logic Programming with Focusing Proofs in Linear Logic
• On the meaning of logical rules. II: Multiplicatives and additives
• Proof normalization modulo
• Superdeduction at Work
• Theorem proving modulo
• Truth Values Algebras and Proof Normalization
• Typed Lambda Calculi and Applications
• Unbounded Proof-Length Speed-Up in Deduction Modulo

Cited in

(5)

• A Simple Proof That Super-Consistency Implies Cut Elimination
• A simple proof that super-consistency implies cut elimination
• scientific article; zbMATH DE number 2086373 (Why is no real title available?)
• Superdeduction in \(\bar{\lambda}\mu\tilde{\mu}\)
• Focusing in Orthologic

This page was built for publication: Axiom Directed Focusing

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