@misc(BarFT-SMTLIB,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2016},
 title        = {The Satisfiability Modulo Theories Library ({SMT-LIB})},
 howpublished = {{\tt www.SMT-LIB.org}},
)
@inproceedings(barrett2006splitting,
 author       = {Clark Barrett and Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli},
 year         = {2006},
 title        = {Splitting on Demand in {SAT} Modulo Theories},
 booktitle    = {International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06)},
 publisher    = {Springer},
 pages        = {512--526},
 doi          = {10.1007/11916277_35},
)
@inproceedings(vssmt,
 author       = {Florian Corzilius and Erika {\'A}brah{\'a}m},
 year         = {2011},
 title        = {Virtual Substitution for {SMT}-Solving},
 booktitle    = {International Symposium on Fundamentals of Computation Theory (FCT'11)},
 publisher    = {Springer},
 pages        = {360--371},
 doi          = {10.1007/978-3-642-22953-4_31},
)
@inproceedings(corziliusSMTRAT2015,
 author       = {Florian Corzilius and Gereon Kremer and Sebastian Junges and Stefan Schupp and Erika {\'A}brah{\'a}m},
 year         = {2015},
 title        = {{SMT-RAT}: {A}n Open Source {C}++ Toolbox for Strategic and Parallel {SMT} Solving},
 booktitle    = {International Conference on Theory and Applications of Satisfiability Testing (SAT'15)},
 publisher    = {Springer},
 pages        = {360--368},
 doi          = {10.1007/978-3-319-24318-4_26},
)
@inproceedings(cottonNatural2010,
 author       = {Scott Cotton},
 year         = {2010},
 title        = {Natural {Domain} {SMT}: {A} {Preliminary} {Assessment}},
 booktitle    = {International Conference on Formal {Modeling} and {Analysis} of {Timed} {Systems} ({FORMATS'10})},
 publisher    = {Springer},
 pages        = {77--91},
 doi          = {10.1007/978-3-642-15297-9_8},
)
@book(dantzig1998linear,
 author       = {George Bernard Dantzig},
 year         = {1998},
 title        = {Linear Programming and Extensions},
 volume       = {48},
 publisher    = {Princeton University Press},
 doi          = {10.1515/9781400884179},
)
@article(dutertre2006integrating,
 author       = {Bruno Dutertre and De Moura, Leonardo},
 year         = {2006},
 title        = {Integrating Simplex with {DPLL(T)}},
 journal      = {Computer Science Laboratory, SRI International, Tech. Rep. SRI-CSL-06-01},
)
@article(farkas1902theorie,
 author       = {Julius Farkas},
 year         = {1902},
 title        = {Theorie der einfachen {U}ngleichungen},
 journal      = {Journal f{\"u}r die reine und angewandte Mathematik (Crelles Journal)},
 volume       = {1902},
 number       = {124},
 pages        = {1--27},
 doi          = {10.1515/crll.1902.124.1},
)
@article(fourier1827analyse,
 author       = {Jean Baptiste Joseph Fourier},
 year         = {1827},
 title        = {Analyse des travaux de l’Acad{\'e}mie Royale des Sciences pendant l’ann{\'e}e 1824},
 journal      = {Partie math{\'e}matique},
)
@incollection(imbert1990redundant,
 author       = {Jean-Louis Imbert},
 year         = {1990},
 title        = {About Redundant Inequalities Generated by {F}ourier's Algorithm},
 booktitle    = {International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'90)},
 publisher    = {Elsevier},
 pages        = {117--127},
 doi          = {10.1016/B978-0-444-88771-9.50019-2},
)
@inproceedings(imbert1993fourier,
 author       = {Jean-Louis Imbert},
 year         = {1993},
 title        = {Fourier's Elimination: {W}hich to Choose?},
 booktitle    = {International Conference on Principles and Practice of Constraint Programming (PPCP'93)},
 volume       = {1},
 publisher    = {Citeseer},
 pages        = {117--129},
)
@inproceedings(JingComplexityFME,
 author       = {Rui-Juan Jing and Moreno-Maza, Marc and Delaram Talaashrafi},
 year         = {2020},
 title        = {Complexity Estimates for {F}ourier-{M}otzkin Elimination},
 booktitle    = {Computer Algebra in Scientific Computing (CASC'20)},
 publisher    = {Springer},
 pages        = {282--306},
 doi          = {10.1007/978-3-030-60026-6_16},
)
@article(KHACHIYAN198053,
 author       = {Leonid Genrikhovich Khachiyan},
 year         = {1980},
 title        = {Polynomial Algorithms in Linear Programming},
 journal      = {{USSR} Computational Mathematics and Mathematical Physics},
 volume       = {20},
 number       = {1},
 pages        = {53--72},
 doi          = {10.1016/0041-5553(80)90061-0},
)
@inproceedings(soisimplex,
 author       = {Tim King and Clark Barrett and Bruno Dutertre},
 year         = {2013},
 title        = {Simplex with Sum of Infeasibilities for {SMT}},
 booktitle    = {Formal Methods in Computer-Aided Design (FMCAD'13)},
 pages        = {189--196},
 doi          = {10.1109/FMCAD.2013.6679409},
)
@inproceedings(korovin2014towards,
 author       = {Konstantin Korovin and Marek Kosta and Thomas Sturm},
 year         = {2014},
 title        = {Towards Conflict-driven Learning for Virtual Substitution},
 booktitle    = {International Workshop on Computer Algebra in Scientific Computing (CASC'14)},
 publisher    = {Springer},
 pages        = {256--270},
 doi          = {10.1007/978-3-319-10515-4_19},
)
@inproceedings(korovinConflict2009,
 author       = {Konstantin Korovin and Nestan Tsiskaridze and Andrei Voronkov},
 year         = {2009},
 title        = {Conflict {Resolution}},
 booktitle    = {Principles and {Practice} of {Constraint} {Programming} (CP'09)},
 publisher    = {Springer},
 pages        = {509--523},
 doi          = {10.1007/978-3-642-04244-7_41},
)
@inproceedings(korovinSolving2011,
 author       = {Konstantin Korovin and Andrei Voronkov},
 year         = {2011},
 title        = {Solving {Systems} of {Linear} {Inequalities} by {Bound} {Propagation}},
 booktitle    = {Conference on Automated {Deduction} ({CADE}'23)},
 publisher    = {Springer},
 pages        = {369--383},
 doi          = {10.1007/978-3-642-22438-6_28},
)
@article(lemke1954dual,
 author       = {Carlton E. Lemke},
 year         = {1954},
 title        = {The Dual Method of Solving the Linear Programming Problem},
 journal      = {Naval Research Logistics Quarterly},
 volume       = {1},
 number       = {1},
 pages        = {36--47},
 doi          = {10.1002/nav.3800010107},
)
@inproceedings(li2021choosing,
 author       = {Haokun Li and Bican Xia and Huiying Zhang and Tao Zheng},
 year         = {2021},
 title        = {Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure},
 booktitle    = {International Symposium on Symbolic and Algebraic Computation (ISSAC'21)},
 publisher    = {ACM},
 pages        = {281--288},
 doi          = {10.1145/3452143.3465520},
)
@article(loosApplyingLinearQuantifier1993,
 author       = {R{\"u}diger Loos and Volker Weispfenning},
 year         = {1993},
 title        = {Applying Linear Quantifier Elimination},
 journal      = {The Computer Journal},
 volume       = {36},
 number       = {5},
 pages        = {450--462},
 doi          = {10.1093/comjnl/36.5.450},
)
@book(luenberger1984linear,
 author       = {David G Luenberger and Yinyu Ye},
 year         = {1984},
 title        = {Linear and Nonlinear Programming},
 volume       = {2nd edition},
 publisher    = {Springer},
 doi          = {10.1007/978-3-030-85450-8},
)
@inproceedings(mcmillanGeneralizing2009,
 author       = {Kenneth L. McMillan and Andreas Kuehlmann and Mooly Sagiv},
 year         = {2009},
 title        = {Generalizing {DPLL} to {Richer} {Logics}},
 booktitle    = {International Conference on Computer {Aided} {Verification} {(CAV'09)}},
 publisher    = {Springer},
 pages        = {462--476},
 doi          = {10.1007/978-3-642-02658-4_35},
)
@book(motzkin1936beitrage,
 author       = {Theodore Samuel Motzkin},
 year         = {1936},
 title        = {Beitr{\"a}ge zur {T}heorie der linearen {U}ngleichungen},
 publisher    = {Azriel},
)
@inproceedings(nalbach2021extending,
 author       = {Jasper Nalbach and Erika {\'A}brah{\'a}m and Gereon Kremer},
 year         = {2021},
 title        = {Extending the Fundamental Theorem of Linear Programming for Strict Inequalities},
 booktitle    = {International Symposium on Symbolic and Algebraic Computation (ISSAC'21)},
 publisher    = {ACM},
 pages        = {313--320},
 doi          = {10.1145/3452143.3465538},
)
@misc(nalbach2023fmplex,
 author       = {Jasper Nalbach and Valentin Promies and Erika Ábrahám and Paul Kobialka},
 year         = {2023},
 title        = {FMplex: A Novel Method for Solving Linear Real Arithmetic Problems},
 eprint       = {2309.03138},
)
@inproceedings(nipkowLinearQuantifierElimination2008a,
 author       = {Tobias Nipkow},
 year         = {2008},
 title        = {Linear Quantifier Elimination},
 booktitle    = {Internation Joint Conference on Automated Reasoning (IJCAR'08)},
 publisher    = {Springer},
 pages        = {18--33},
 doi          = {10.1007/978-3-540-71070-7_3},
)
@article(weispfenning1997quantifier,
 author       = {Volker Weispfenning},
 year         = {1997},
 title        = {Quantifier Elimination for Real Algebra—the Quadratic Case and Beyond},
 journal      = {Applicable Algebra in Engineering, Communication and Computing},
 volume       = {8},
 number       = {2},
 pages        = {85--101},
 doi          = {10.1007/s002000050055},
)