Unbounded Proof-Length Speed-Up in Deduction Modulo

DOI10.1007/978-3-540-74915-8_37MaRDI QIDQ3608434zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

proof theoryarithmeticrewritinghigher-order logic

Mathematics Subject Classification ID

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

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

Cited in

(4)

• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Axiom Directed Focusing
• 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)