Unbounded Proof-Length Speed-Up in Deduction Modulo

DOI10.1007/978-3-540-74915-8_37zbMath1179.03059OpenAlexW1490144336MaRDI QIDQ3608434

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

arithmetichigher-order logicproof theoryrewriting

Mathematics Subject Classification ID

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

Related Items (2)

Regaining cut admissibility in deduction modulo using abstract completion ⋮ Axiom Directed Focusing

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