Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo

DOI10.1007/978-3-642-45221-5_20MaRDI QIDQ2870135zbMATH OpenOpenAlexFDO

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

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

automated theorem provingdeduction moduloDeduktiproof checkingrewritingtableauxZenon

Mathematics Subject Classification ID

Recommendations

• A discrete solution for the paradox of Achilles and the tortoise
• Achilles and the tortoise climbing up the hyper-arithmetical hierarchy
• Zeno, Hercules and the Hydra: downward rational termination is Ackermannian
• Achilles and the tortoise climbing up the arithmetical hierarchy
• Achilles and the tortoise climbing up the arithmetical hierarchy
• scientific article; zbMATH DE number 7686231
• Experimenting with deduction modulo
• Unbounded Proof-Length Speed-Up in Deduction Modulo
• scientific article; zbMATH DE number 1231675
• Running modulus recursions

Cited in

(15)

• Zenon
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• GRUNGE: a grand unified ATP challenge
• Automatically proving equivalence by type-safe reflection
• Zeno: an automated prover for properties of recursive data structures
• Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
• Soundly proving B method formulæ using typed sequent calculus
• ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
• CTL model checking in deduction modulo
• Integrating simplex with tableaux
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Unbounded Proof-Length Speed-Up in Deduction Modulo
• A Polymorphic Vampire
• scientific article; zbMATH DE number 7686231 (Why is no real title available?)
• Reconstruction of SMT proofs with Lambdapi

Describes a project that uses

Uses Software

• TPTP
• dedukti
• BWare

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

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