Unbounded Proof-Length Speed-Up in Deduction Modulo

DOI10.1007/978-3-540-74915-8_37zbMATH Open1179.03059OpenAlexW1490144336MaRDI QIDQ3608434FDOQ3608434

Authors: Guillaume Burel 

Publication date: 5 March 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00138195v3/file/speedup_full.pdf

Recommendations

• Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
• On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Polynomially and superexponentially shorter proofs in fragments of arithmetic
• Theorem proving modulo

zbMATH Keywords

proof theoryarithmeticrewritinghigher-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Cited In (4)

• Axiom Directed Focusing
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Fast LCF-Style Proof Reconstruction for Z3
• Regaining cut admissibility in deduction modulo using abstract completion

This page was built for publication: Unbounded Proof-Length Speed-Up in Deduction Modulo

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