@article{10.1093/comjnl/36.5.450,
    Abstract = {{The linear quantifier elimination algorithm for ordered fields in [15] is applicable to a wide range of examples involving even non-linear parameters. The Skolem sets of the original algorithm are generalized to elimination sets whose size is linear in the number of atomic formulas, whereas the size of Skolem sets is quadratic in this number. Elimination sets may contain non-standard terms which enter the computation symbolically. Many cases can be treated by special methods improving further the empirical computing times.}},
    Author = {Loos, R. and Weispfenning, V.},
    EPrint = {http://oup.prod.sis.lan/comjnl/article-pdf/36/5/450/1105730/360450.pdf},
    File = {360450 (0) - a - a - z.pdf},
    ISSN = {0010-4620},
    Journal = {The Computer Journal},
    Month = {01},
    Number = {5},
    Pages = {450-462},
    Title = {{Applying Linear Quantifier Elimination}},
    URL = {https://doi.org/10.1093/comjnl/36.5.450},
    Volume = {36},
    Year = {1993},
    bdsk-url-1 = {https://doi.org/10.1093/comjnl/36.5.450},
    date-added = {2019-04-29 14:29:19 +0200},
    date-modified = {2019-04-29 14:29:19 +0200},
    doi = {10.1093/comjnl/36.5.450}
}

@article{10.1093/comjnl/36.5.450, Abstract = {{The linear quantifier elimination algorithm for ordered fields in [15] is applicable to a wide range of examples involving even non-linear parameters. The Skolem sets of the original algorithm are generalized to elimination sets whose size is linear in the number of atomic formulas, whereas the size of Skolem sets is quadratic in this number. Elimination sets may contain non-standard terms which enter the computation symbolically. Many cases can be treated by special methods improving further the empirical computing times.}}, Author = {Loos, R. and Weispfenning, V.}, EPrint = {http://oup.prod.sis.lan/comjnl/article-pdf/36/5/450/1105730/360450.pdf}, File = {360450 (0) - a - a - z.pdf}, ISSN = {0010-4620}, Journal = {The Computer Journal}, Month = {01}, Number = {5}, Pages = {450-462}, Title = {{Applying Linear Quantifier Elimination}}, URL = {https://doi.org/10.1093/comjnl/36.5.450}, Volume = {36}, Year = {1993}, bdsk-url-1 = {https://doi.org/10.1093/comjnl/36.5.450}, date-added = {2019-04-29 14:29:19 +0200}, date-modified = {2019-04-29 14:29:19 +0200}, doi = {10.1093/comjnl/36.5.450} }