Experimenting with Deduction Modulo

DOI10.1007/978-3-642-22438-6_14zbMath1341.68185OpenAlexW182131396MaRDI QIDQ5200022

Guillaume Burel

Publication date: 29 July 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_14

Mathematics Subject Classification ID

Related Items

CTL Model Checking in Deduction Modulo ⋮ FoCaLiZe and Dedukti to the rescue for proof interoperability ⋮ Unnamed Item ⋮ Clausal presentation of theories in deduction modulo ⋮ GRUNGE: a grand unified ATP challenge

Uses Software

• VAMPIRE
• SPASS
• TPTP
• iProver

Cites Work

• Unnamed Item
• Unnamed Item
• Term rewriting for normalization by evaluation.
• Theorem proving modulo
• Regaining cut admissibility in deduction modulo using abstract completion
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• HOL-λσ: an intentional first-order expression of higher-order logic
• Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Polarized Resolution Modulo
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Embedding Deduction Modulo into a Prover
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Automated Reasoning
• A Semantic Completeness Proof for TaMeD
• Term Rewriting and Applications