A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm

Katherine Cordwell, Yong Kiam Tan, André Platzer. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. In Liron Cohen 0001, Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). Volume 193 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [doi]

@inproceedings{CordwellTP21-0,
  title = {A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm},
  author = {Katherine Cordwell and Yong Kiam Tan and André Platzer},
  year = {2021},
  doi = {10.4230/LIPIcs.ITP.2021.14},
  url = {https://doi.org/10.4230/LIPIcs.ITP.2021.14},
  researchr = {https://researchr.org/publication/CordwellTP21-0},
  cites = {0},
  citedby = {0},
  booktitle = {12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  editor = {Liron Cohen 0001 and Cezary Kaliszyk},
  volume = {193},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-188-7},
}