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

DOI10.2168/LMCS-7(1:3)2011MaRDI QIDQ3003304zbMATH OpenFDO

Authors 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)

Recommendations

• Model-theoretic methods of analysis of computer arithmetic
• Efficient Exact Arithmetic over Constructive Reals
• Modular termination and combinability for superposition modulo counter arithmetic
• An efficient representation of arithmetic for term rewriting
• Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
• A practical approach to satisfiability modulo linear integer arithmetic
• Publication:3199395
• Modular bisimulation theory for computations and values
• Self-verified extension of affine arithmetic to arbitrary order
• On Presburger arithmetic extended with modulo counting quantifiers

Cited in

(4)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• A Finite First-Order Theory of Classes
• Experimenting with deduction modulo
• Unbounded Proof-Length Speed-Up in Deduction Modulo

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)