DROPS

Document

Short Paper

DOI: 10.4230/LIPIcs.ITP.2026.32

Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)

Authors: Aeacus Sheng, Wenda Li, and Paul B. Jackson

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

Real root isolation is a fundamental subroutine in computer algebra, with applications ranging from algebraic number arithmetic to solving polynomial systems. Modern implementations typically employ subdivision methods based on root counting via Descartes' rule of signs. In contrast, most existing formally verified root isolation procedures rely on Sturm's theorem for root counting, leading to a noticeable gap between practical implementations and formally verified approaches. We take an initial step towards efficient verified real root isolation by formally verifying two simple algorithms based on Descartes' rule of signs: a classical bisection procedure and a Newton-accelerated variant. In this paper, we describe the algorithms, present formal proofs of termination, soundness, and completeness, and discuss our code-generation efforts. Brief experiments show promising performance improvements over existing formally verified algorithms in Isabelle/HOL.

Cite as

Aeacus Sheng, Wenda Li, and Paul B. Jackson. Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 32:1-32:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{sheng_et_al:LIPIcs.ITP.2026.32,
  author =	{Sheng, Aeacus and Li, Wenda and Jackson, Paul B.},
  title =	{{Faster Verified Real Root Isolation with Descartes' Rule of Signs}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{32:1--32:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.32},
  URN =		{urn:nbn:de:0030-drops-270068},
  doi =		{10.4230/LIPIcs.ITP.2026.32},
  annote =	{Keywords: Isabelle/HOL, Real root isolation, Descartes' rule of signs}
}

Document

DOI: 10.4230/DagSemProc.10161.3

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops

Authors: Grant Olney Passmore, Leonardo de Moura, and Paul B. Jackson

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)

Abstract

We present novel Gr"obner basis algorithms based on saturation loops used by modern superposition theorem provers. We illustrate the practical value of the algorithms through an experimental implementation within the Z3 SMT solver.

Cite as

Grant Olney Passmore, Leonardo de Moura, and Paul B. Jackson. Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{passmore_et_al:DagSemProc.10161.3,
  author =	{Passmore, Grant Olney and de Moura, Leonardo and Jackson, Paul B.},
  title =	{{Gr\"{o}bner Basis Construction Algorithms Based on Theorem Proving Saturation Loops}},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.3},
  URN =		{urn:nbn:de:0030-drops-27345},
  doi =		{10.4230/DagSemProc.10161.3},
  annote =	{Keywords: Groebner bases, ideal theory, automated theorem proving, SMT solvers}
}

Search Results

Documents authored by Jackson, Paul B.

Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)

Abstract

Cite as

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops

Abstract

Cite as

Thanks for your feedback!

Could not send message