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

DOI10.2168/LMCS-7(1:3)2011zbMATH Open1218.03007MaRDI QIDQ3003304FDOQ3003304

Guillaume Burel

Publication date: 26 May 2011

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

zbMATH Keywords

proof complexityarithmeticterm rewritinghigher-order logicdeduction moduloproof-length speed-ups

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Second- and higher-order arithmetic and fragments (03F35)

Cited In (2)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Experimenting with Deduction Modulo

Recommendations

• A practical approach to satisfiability modulo linear integer arithmetic 👍 👎
• Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions 👍 👎
• Modular Bisimulation Theory for Computations and Values 👍 👎
• Efficient Exact Arithmetic over Constructive Reals 👍 👎
• Modular Termination and Combinability for Superposition Modulo Counter Arithmetic 👍 👎
• On Presburger Arithmetic Extended with Modulo Counting Quantifiers 👍 👎
• An efficient representation of arithmetic for term rewriting 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎

This page was built for publication: Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo

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