A Verified Proof Checker for Metric First-Order Temporal Logic
by Andrei Herasimau, Jonathan Julian Huerta y Munive 📧, Leonardo Lima, Martin Raszyk 📧 and Dmitriy Traytel 🌐
diff --git a/web/authors/herasimau/index.html b/web/authors/herasimau/index.html --- a/web/authors/herasimau/index.html +++ b/web/authors/herasimau/index.html @@ -1,139 +1,138 @@
Jose Divasón 🌐, Sebastiaan J. C. Joosten 📧, René Thiemann 📧 and Akihisa Yamada 📧
October 14, 2016
We formalize the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the integer ring modulo p^k, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle’s recent addition of local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.
Palle Raabjerg 📧, Johannes Åman Pohjola 📧 and Tjark Weber 📧
March 27, 2024
June 21, 2016
In this work, we define the Catalan numbers Cn +
In this work, we define the Catalan numbers $C_n$ and prove several equivalent definitions (including some closed-form formulae). We also show one of their applications (counting the number -of binary trees of size n), prove the asymptotic growth -approximation Cn ∼ 4n / (√π · -n1.5), and provide reasonably efficient executable +of binary trees of size $n$), prove the asymptotic growth +approximation $C_n \sim \frac{4^n}{\sqrt{\pi}\, n^{3/2}}$, and provide reasonably efficient executable code to compute them.
The derivation of the closed-form formulae uses algebraic manipulations of the ordinary generating function of the Catalan numbers, and the asymptotic approximation is then done using generalised binomial coefficients and the Gamma -function. Thanks to these highly non-elementary mathematical tools, -the proofs are very short and simple.
July 18, 2022
April 16, 2024
February 15, 2024
February 15, 2022
Christian Sternagel 📧 and René Thiemann 🌐
February 6, 2018
April 3, 2023
Asta Halkjær From 🌐 and Jørgen Villadsen 🌐
September 13, 2022
René Thiemann 📧 and Akihisa Yamada 📧 with contributions from Alexander Bentkamp 📧
August 21, 2015
Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.
To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and prove the result that every complex matrix has a Jordan normal form using a constructive prove via Schur decomposition.
The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices, and its main advantage is its close connection to the HMA-representation which allowed us to easily adapt existing proofs on determinants.
All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.
Thibault Dardinier, Lukas Heimes, Martin Raszyk 📧, Joshua Schneider 📧 and Dmitriy Traytel 🌐
April 9, 2020
Andrei Herasimau, Jonathan Julian Huerta y Munive 📧, Leonardo Lima, Martin Raszyk 📧 and Dmitriy Traytel 🌐
April 16, 2024
Joshua Schneider 📧 and Dmitriy Traytel 🌐
July 4, 2019
René Thiemann 📧 and Akihisa Yamada 📧
January 29, 2016
As side products, we developed division algorithms for polynomials over integral domains, as well as primality-testing and prime-factorization algorithms for integers.
Julius Michaelis 🌐, Max W. Haslbeck 🌐, Peter Lammich 🌐 and Lars Hupel 🌐
April 27, 2016
September 22, 2023
Christian Sternagel 📧 and René Thiemann 📧
July 29, 2014
March 26, 2024
- Christian Sternagel 📧 and René Thiemann 📧 + Christian Sternagel 📧, René Thiemann 📧 and Akihisa Yamada 📧
October 3, 2014
The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed and we encourage companion AFP submissions to conference and journal publications. To cite an entry, please use the preferred citation style.
A development version of the archive is available as well.
813 | Entries |
486 | Authors |
-<<<<<<< working copy - ~254,500 -======= - ~258,500 ->>>>>>> merge rev + ~258,900 | Lemmas |
-<<<<<<< working copy - ~4,124,100 -======= - ~4,183,400 ->>>>>>> merge rev + ~4,188,400 | Lines of Code |
Name | Used by ? entries | ||
---|---|---|---|
1. | List-Index | 23 | |
2. | Collections | 19 | |
3. | Show | -16 | +17 |
4. | Coinductive | 15 | |
5. | Jordan_Normal_Form | 15 | |
6. | Deriving | 14 | |
7. | Polynomial_Factorization | -13 | +14 |
8. | Polynomial_Interpolation | 12 | |
9. | Regular-Sets | 12 | |
10. | Landau_Symbols | 11 | |
11. | Abstract-Rewriting | 10 | |
12. | Automatic_Refinement | 10 |
ACM: Theory of computation~Data structures design and analysis
AMS: Computer science / Theory of data / Data structures
ACM: Software and its engineering~Functional languages
AMS: Computer science / Theory of software / Functional programming and lambda calculus
AMS: Game theory, economics, finance, and other social and behavioral sciences
+