caa a22 4500 463182693 CHVBK 20180406164843.0 cr unu---uuuuu 170326e20070501xx s 000 0 eng 10.1007/s10817-007-9066-1 doi (NATIONALLICENCE)springer-10.1007/s10817-007-9066-1 A Decision Procedure for Linear "Big O” Equations [Elektronische Daten] [Jeremy Avigad, Kevin Donnelly] Let F be the set of functions from an infinite set, S, to an ordered ring, R. For f, g, and h in F, the assertion f = g + O(h) means that for some constant C, |f(x) − g(x)| ≤C |h(x)| for every x in S. Let L be the first-order language with variables ranging over such functions, symbols for 0, +, −, min , max , and absolute value, and a ternary relation f = g + O(h). We show that the set of quantifier-free formulas in this language that are valid in the intended class of interpretations is decidable and does not depend on the underlying set, S, or the ordered ring, R. If R is a subfield of the real numbers, we can add a constant 1 function, as well as multiplication by constants from any computable subfield. We obtain further decidability results for certain situations in which one adds symbols denoting the elements of a fixed sequence of functions of strictly increasing rates of growth. Springer Science+Business Media, Inc., 2007 Decision procedures nationallicence Asymptotic equations nationallicence Big O nationallicence Avigad Jeremy Department of Philosophy, Carnegie Mellon University, 15213, Pittsburgh, PA, USA aut Donnelly Kevin Department of Computer Science, Boston University, 02215, Boston, MA, USA aut Journal of Automated Reasoning Kluwer Academic Publishers 38/4(2007-05-01), 353-373 0168-7433 38:4<353 2007 38 10817 https://doi.org/10.1007/s10817-007-9066-1 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-007-9066-1 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Avigad Jeremy Department of Philosophy, Carnegie Mellon University, 15213, Pittsburgh, PA, USA aut NATIONALLICENCE 700 1- Donnelly Kevin Department of Computer Science, Boston University, 02215, Boston, MA, USA aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/4(2007-05-01), 353-373 0168-7433 38:4<353 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer