Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
From MaRDI portal
Publication:3003304
DOI10.2168/LMCS-7(1:3)2011zbMath1218.03007MaRDI QIDQ3003304
Publication date: 26 May 2011
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
arithmetic; higher-order logic; term rewriting; proof complexity; deduction modulo; proof-length speed-ups
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, First-order automated reasoning with theories: when deduction modulo theory meets practice