Automating Theories in Intuitionistic Logic

DOI10.1007/978-3-642-04222-5_11zbMath1193.03026OpenAlexW1548268448MaRDI QIDQ3655199

Guillaume Burel

Publication date: 7 January 2010

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04222-5_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (2)

Regaining cut admissibility in deduction modulo using abstract completion ⋮ Automating Theories in Intuitionistic Logic

Uses Software

• ILTP

Cites Work

• The ILTP problem library for intuitionistic logic
• Theorem proving modulo
• Untersuchungen über das logische Schliessen. I
• The Skolem method in intuitionistic calculi
• The axioms of constructive geometry
• Regaining cut admissibility in deduction modulo using abstract completion
• HOL-λσ: an intentional first-order expression of higher-order logic
• On Constructive Cut Admissibility in Deduction Modulo
• A Finite First-Order Theory of Classes
• On Skolemization in constructive theories
• Automating Theories in Intuitionistic Logic
• Term Rewriting and All That
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Automating Theories in Intuitionistic Logic