Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo

DOI10.1007/978-3-642-45221-5_20zbMath1406.68105OpenAlexW129696796MaRDI QIDQ2870135

Pierre Halmagrand, Olivier Hermant, Damien Doligez, Frédéric Gilbert, David Delahaye

Publication date: 17 January 2014

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

tableauxrewritingautomated theorem provingproof checkingdeduction moduloZenonDedukti

Mathematics Subject Classification ID

Related Items (9)

Automatically proving equivalence by type-safe reflection ⋮ A Polymorphic Vampire ⋮ CTL Model Checking in Deduction Modulo ⋮ Integrating Simplex with Tableaux ⋮ Soundly Proving B Method Formulæ Using Typed Sequent Calculus ⋮ ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ GRUNGE: a grand unified ATP challenge ⋮ Zenon

Uses Software

• TPTP
• BWare
• dedukti

This page was built for publication: Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo