Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo

DOI10.2168/LMCS-7(1:3)2011zbMath1218.03007MaRDI QIDQ3003304

Guillaume Burel

Publication date: 26 May 2011

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

arithmetic; higher-order logic; term rewriting; proof complexity; deduction modulo; proof-length speed-ups

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

68Q42: Grammars and rewriting systems

03F35: Second- and higher-order arithmetic and fragments

03F20: Complexity of proofs

Related Items

Experimenting with Deduction Modulo