@article{Nipkow2010,
    Abstract = {This paper presents verified quantifier elimination procedures for dense linear orders (two of them novel), for real and for integer linear arithmetic. All procedures are defined and verified in the theorem prover Isabelle/HOL, are executable and can be applied to HOL formulae themselves (by reflection). The formalization of the different theories is highly modular.},
    Author = {Nipkow, Tobias},
    File = {art\%3A10.1007\%2Fs10817-010-9183-0 (0) - a - a - n.pdf},
    ISSN = {1573-0670},
    Journal = {Journal of Automated Reasoning},
    Number = {2},
    Pages = {189--212},
    Title = {Linear Quantifier Elimination},
    URL = {http://dx.doi.org/10.1007/s10817-010-9183-0},
    Volume = {45},
    Year = {2010},
    bdsk-url-1 = {http://dx.doi.org/10.1007/s10817-010-9183-0},
    date-added = {2017-03-31 11:41:51 +0000},
    date-modified = {2017-03-31 11:41:51 +0000},
    file-2 = {ijcar08 (0) - a - a - n.pdf},
    doi = {10.1007/s10817-010-9183-0}
}

@article{Nipkow2010, Abstract = {This paper presents verified quantifier elimination procedures for dense linear orders (two of them novel), for real and for integer linear arithmetic. All procedures are defined and verified in the theorem prover Isabelle/HOL, are executable and can be applied to HOL formulae themselves (by reflection). The formalization of the different theories is highly modular.}, Author = {Nipkow, Tobias}, File = {art\%3A10.1007\%2Fs10817-010-9183-0 (0) - a - a - n.pdf}, ISSN = {1573-0670}, Journal = {Journal of Automated Reasoning}, Number = {2}, Pages = {189--212}, Title = {Linear Quantifier Elimination}, URL = {http://dx.doi.org/10.1007/s10817-010-9183-0}, Volume = {45}, Year = {2010}, bdsk-url-1 = {http://dx.doi.org/10.1007/s10817-010-9183-0}, date-added = {2017-03-31 11:41:51 +0000}, date-modified = {2017-03-31 11:41:51 +0000}, file-2 = {ijcar08 (0) - a - a - n.pdf}, doi = {10.1007/s10817-010-9183-0} }