A decision procedure for linear ``big O equations

DOI10.1007/s10817-007-9066-1zbMath1122.03004arXivcs/0701073OpenAlexW2140507616MaRDI QIDQ2642465

Jeremy Avigad, Kevin P. Donnelly

Publication date: 17 August 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/cs/0701073

zbMATH Keywords

Asymptotic equationsDecision proceduresBig O

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (1)

Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Uses Software

• Coq
• ML
• Isabelle/HOL
• PVS
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A new polynomial-time algorithm for linear programming
• The complexity of linear problems in fields
• Isabelle/HOL. A proof assistant for higher-order logic
• Applying Linear Quantifier Elimination
• Principles of Constraint Programming
• A formally verified proof of the prime number theorem
• Automated Reasoning
• Combining decision procedures for the reals

This page was built for publication: A decision procedure for linear ``big O equations