5 Search Results for "Immler, Fabian"

Document
DOI: 10.4230/LIPIcs.ITP.2025.3
A Formal Proof of Complexity Bounds on Diophantine Equations

Authors: Jonas Bayer and Marco David

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We present a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalization of our own work in number theory [Jonas Bayer et al., 2025]. Hilbert’s Tenth Problem was answered negatively by Yuri Matiyasevich, who showed that there is no general algorithm to decide whether an arbitrary Diophantine equation has a solution. However, the problem remains open when generalized to the field of rational numbers, or contrarily, when restricted to Diophantine equations with bounded complexity, characterized by the number of variables ν and the degree δ. If every Diophantine set can be represented within the bounds (ν, δ), we say that this pair is universal, and it follows that the corresponding class of equations is undecidable. In a separate mathematics article, we have determined the first non-trivial universal pair for the case of integer unknowns. In this paper, we contribute a formal verification of this new result. In doing so, we markedly extend the Isabelle AFP entry on multivariate polynomials [Christian Sternagel et al., 2010], formalize parts of a number theory textbook [Melvyn B. Nathanson, 1996], and develop classical theory on Diophantine equations [Yuri Matiyasevich and Julia Robinson, 1975] in Isabelle. In addition, our work includes metaprogramming infrastructure designed to efficiently handle complex definitions of multivariate polynomials. Our mathematical draft has been formalized while the mathematical research was ongoing, and benefited largely from the help of the theorem prover. We reflect on how the close collaboration between mathematician and computer is an uncommon but promising modus operandi.
Cite as

Jonas Bayer and Marco David. A Formal Proof of Complexity Bounds on Diophantine Equations. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bayer_et_al:LIPIcs.ITP.2025.3,
  author =	{Bayer, Jonas and David, Marco},
  title =	{{A Formal Proof of Complexity Bounds on Diophantine Equations}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.3},
  URN =		{urn:nbn:de:0030-drops-246023},
  doi =		{10.4230/LIPIcs.ITP.2025.3},
  annote =	{Keywords: Diophantine Equations, Hilbert’s Tenth Problem, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.24
Formally Verifying a Vertical Cell Decomposition Algorithm

Authors: Yves Bertot and Thomas Portet

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The broad context of this work is the application of formal methods to geometry and robotics. We describe an algorithm to decompose a working area containing obstacles into a collection of safe cells and the formal proof that this algorithm is correct. We expect such an algorithm will be useful to compute safe trajectories. To our knowledge, this is one of the first formalization of such an algorithm to decompose a working space into elementary cells that are suitable for later applications, with the proof of correctness that guarantees that large parts of the working space are safe. Techniques to perform this proof go from algebraic reasoning on coordinates and determinants to sorting. The main difficulty comes from the possible existence of degenerate cases, which are treated in a principled way.
Cite as

Yves Bertot and Thomas Portet. Formally Verifying a Vertical Cell Decomposition Algorithm. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2025.24,
  author =	{Bertot, Yves and Portet, Thomas},
  title =	{{Formally Verifying a Vertical Cell Decomposition Algorithm}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.24},
  URN =		{urn:nbn:de:0030-drops-246222},
  doi =		{10.4230/LIPIcs.ITP.2025.24},
  annote =	{Keywords: Formal Verification, Motion planning, algorithmic geometry}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.18
Formalising New Mathematics in Isabelle: Diagonal Ramsey

Authors: Lawrence C. Paulson

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The formalisation of mathematics is becoming routine, but its value to research mathematicians remains unproven. There are few examples of using proof assistants to verify new work. This paper reports the formalisation - inspired by a Lean one by Bhavik Mehta - of a major new result [Marcelo Campos et al., 2023] about Ramsey numbers. One unexpected finding was a heavy role for computer algebra techniques.
Cite as

Lawrence C. Paulson. Formalising New Mathematics in Isabelle: Diagonal Ramsey. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{paulson:LIPIcs.ITP.2025.18,
  author =	{Paulson, Lawrence C.},
  title =	{{Formalising New Mathematics in Isabelle: Diagonal Ramsey}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.18},
  URN =		{urn:nbn:de:0030-drops-246163},
  doi =		{10.4230/LIPIcs.ITP.2025.18},
  annote =	{Keywords: Isabelle, formalisation of mathematics, Ramsey’s theorem, computer algebra}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.14
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm

Authors: Katherine Cordwell, Yong Kiam Tan, and André Platzer

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
We formalize the univariate fragment of Ben-Or, Kozen, and Reif’s (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR’s algorithm has good potential for parallelism and was designed to be used in practice. Its key insight is a clever recursive procedure that computes the set of all consistent sign assignments for an input set of univariate polynomials while carefully managing intermediate steps to avoid exponential blowup from naively enumerating all possible sign assignments (this insight is fundamental for both the univariate case and the general case). Our proof combines ideas from BKR and a follow-up work by Renegar that are well-suited for formalization. The resulting proof outline allows us to build substantially on Isabelle/HOL’s libraries for algebra, analysis, and matrices. Our main extensions to existing libraries are also detailed.
Cite as

Katherine Cordwell, Yong Kiam Tan, and André Platzer. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{cordwell_et_al:LIPIcs.ITP.2021.14,
  author =	{Cordwell, Katherine and Tan, Yong Kiam and Platzer, Andr\'{e}},
  title =	{{A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.14},
  URN =		{urn:nbn:de:0030-drops-139099},
  doi =		{10.4230/LIPIcs.ITP.2021.14},
  annote =	{Keywords: quantifier elimination, matrix, theorem proving, real arithmetic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.21
Virtualization of HOL4 in Isabelle

Authors: Fabian Immler, Jonas Rädle, and Makarius Wenzel

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We present a novel approach to combine the HOL4 and Isabelle theorem provers: both are implemented in SML and based on distinctive variants of HOL. The design of HOL4 allows to replace its inference kernel modules, and the system infrastructure of Isabelle allows to embed other applications of SML. That is the starting point to provide a virtual instance of HOL4 in the same run-time environment as Isabelle. Moreover, with an implementation of a virtual HOL4 kernel that operates on Isabelle/HOL terms and theorems, we can load substantial HOL4 libraries to make them Isabelle theories, but still disconnected from existing Isabelle content. Finally, we introduce a methodology based on the transfer package of Isabelle to connect the imported HOL4 material to that of Isabelle/HOL.
Cite as

Fabian Immler, Jonas Rädle, and Makarius Wenzel. Virtualization of HOL4 in Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{immler_et_al:LIPIcs.ITP.2019.21,
  author =	{Immler, Fabian and R\"{a}dle, Jonas and Wenzel, Makarius},
  title =	{{Virtualization of HOL4 in Isabelle}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.21},
  URN =		{urn:nbn:de:0030-drops-110760},
  doi =		{10.4230/LIPIcs.ITP.2019.21},
  annote =	{Keywords: Virtualization, HOL4, Isabelle, Isabelle/HOL, Isabelle/ML}
}
  • Refine by Type
  • 5 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2021
  • 1 2019

  • Refine by Author
  • 1 Bayer, Jonas
  • 1 Bertot, Yves
  • 1 Cordwell, Katherine
  • 1 David, Marco
  • 1 Immler, Fabian
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 2 Theory of computation → Higher order logic
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • 1 Mathematics of computing → Combinatorics
  • 1 Software and its engineering → Interoperability
  • Show More...

  • Refine by Keyword
  • 2 Isabelle
  • 2 Isabelle/HOL
  • 1 Diophantine Equations
  • 1 Formal Verification
  • 1 HOL4
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact