Christina Kohl, Aart Middeldorp
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), pp. 197-210, 2023.
pdf 
doi:10.1145/3573105.3575667
Abstract
Several critical pair criteria are known that guarantee confluence of left-linear term rewrite systems. The correctness of most of these have been formalized in a proof assistant. An important exception has been the development closedness criterion of van Oostrom. Its proof requires a high level of understanding about overlapping redexes and descendants as well as several intermediate results related to these concepts. We present a formalization in the proof assistant Isabelle/HOL. The result has been integrated into the certifier CeTA.
BibTex
@inproceedings{CKAM-CPP23, author = "Christina Kohl and Aart Middeldorp", title = "A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems", booktitle = "Proceedings of the 12th International {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs", editors = "Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka and Steve Zdancewic", publisher = "ACM", pages = "197--210", doi = "10.1145/3573105.3575667", year = 2023}
- Details
- Category: Publications 2023
Aart Middeldorp, Alexander Lochmann, Fabian Mitterwallner
Journal of Automated Reasoning 67, 2023.
pdf doi:https://doi.org/10.1007/s10817-023-09661-7
Abstract
The first-order theory of rewriting is decidable for linear variable-separated rewrite systems. We present a new decision procedure which is the basis of FORT, a decision and synthesis tool for properties expressible in the theory. The decision procedure is based on tree automata techniques and verified in Isabelle. Several extensions make the theory more expressive and FORT more versatile. We present a certificate language that enables the output of FORT to be certified by the certifier FORTify generated from the formalization, and we provide extensive experiments.
BibTex
@article{AMALFM-JAR23, author = "Aart Middeldorp and Alexander Lochmann and Fabian Mitterwallner", title = "First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification", journal = "Journal of Automated Reasoning", volume = 67, number = 14, pages = "1--76", year = 2023, doi = "10.1007/s10817-023-09661-7"}
- Details
- Category: Publications 2023
Cezary Kaliszyk and Karol Pąk
Journal of Automated Reasoning 2023.
pdf doi:10.1007/S10817-023-09663-5
Abstract
The Isabelle Higher-order Tarski–Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic concepts independently, which means that the results in the two are disconnected. In this paper, we align significant parts of these two libraries, by defining isomorphisms between their concepts, including the real numbers and algebraic structures. The isomorphisms allow us to transport theorems between the foundations and use the results from the libraries simultaneously.
BibTex
@article{ckkp-jar23, author = {Cezary Kaliszyk and Karol Pąk}, title = {Combining Higher-Order Logic with Set Theory Formalizations}, journal = {J. Autom. Reason.}, volume = {67}, number = {2}, pages = {20}, year = {2023}, url = {https://doi.org/10.1007/s10817-023-09663-5}, doi = {10.1007/S10817-023-09663-5},}
- Details
- Category: Publications 2023
René Thiemann, Elias Wenninger
Archive of Formal Proofs 2023.
pdf doi:10.29007/SLRM Open access AFP entry
Abstract
The Weighted Path Order (WPO) of Yamada is a powerful technique for proving termination. In a previous AFP entry, the WPO was defined and properties of WPO have been formally verified. However, the implementation of WPO was naive, leading to an exponential runtime in the worst case.
Therefore, in this AFP entry we provide a poly-time implementation of WPO. The implementation is based on memoization. Since WPO generalizes the recursive path order (RPO), we also easily derive an efficient implementation of RPO.
BibTex
@article{Efficient_Weighted_Path_Order-AFP, author = {René Thiemann and Elias Wenninger}, title = {A Verified Efficient Implementation of the Weighted Path Order}, journal = {Archive of Formal Proofs}, month = {June}, year = {2023}, note = {\url{https://isa-afp.org/entries/Efficient_Weighted_Path_Order.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 317-328, 2023.
pdf doi:10.29007/SLRM Open access
Abstract
We propose infinite model finding as a new task for SMT-Solving. Model finding has a long-standing tradition in SMT and automated reasoning in general. Yet, most of the current tools are limited to finite models despite the fact that many theories only admit infinite models. This paper shows a variety of such problems and evaluates synthesis approaches on them. Interestingly, state-of-the-art SMT solvers fail even on very small and simple problems. We target such problems by SyGuS tools as well as heuristic approaches.
BibTex
@inproceedings{jpcbmjck-lpar23, author = {Julian Parsert and Chad E. Brown and Mikolas Janota and Cezary Kaliszyk}, editor = {Ruzica Piskac and Andrei Voronkov}, title = {Experiments on Infinite Model Finding in {SMT} Solving}, booktitle = {{LPAR} 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning}, series = {EPiC}, volume = {94}, pages = {317--328}, publisher = {EasyChair}, year = {2023}, url = {https://doi.org/10.29007/slrm}, doi = {10.29007/SLRM},}
- Details
- Category: Publications 2023
Emin Karayel, Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
In Isabelle, randomized algorithms are usually represented using probability mass functions (PMFs), with which it is possible to verify their correctness, particularly properties about the distribution of their result. However, that approach does not provide a way to generate executable code for such algorithms. In this entry, we introduce a new monad for randomized algorithms, for which it is possible to generate code and simultaneously reason about the correctness of randomized algorithms. The latter works by a Scott-continuous monad morphism between the newly introduced random monad and PMFs. On the other hand, when supplied with an external source of random coin flips, the randomized algorithms can be executed.
BibTex
@article{Executable_Randomized_Algorithms-AFP, author = {Emin Karayel and Manuel Eberl}, title = {Executable Randomized Algorithms}, journal = {Archive of Formal Proofs}, month = {June}, year = {2023}, note = {\url{https://isa-afp.org/entries/Executable_Randomized_Algorithms.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Nao Hirokawa, Aart Middeldorp
Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 260, pp. 22:1-12:16, 2023.
pdf doi:10.4230/LIPIcs.FSCD.2023.12
Abstract
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO.
BibTex
@inproceedings{NHAM-FSCD23, author = "Nao Hirokawa and Aart Middeldorp", title = "Hydra Battles and {AC} Termination", booktitle = "Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction", editor = "Marco Gaboardi and Femke van Raamsdonk", series = "Leibniz International Proceedings in Informatics", volume = 260, pages = "12:1--12:16", year = 2023, doi = "10.4230/LIPIcs.FSCD.2023.12"}
- Details
- Category: Publications 2023
Jan Jakubův, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
14th International Conference on Interactive Theorem Proving, pp. 19:1-19:22, 2023.
pdf doi:10.4230/LIPIcs.ITP.2023.19
Abstract
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.
BibTex
@inproceedings{jjkczgckmobpssmsju-itp23, author = {Jan Jakubuv and Karel Chvalovsk{\'{y}} and Zarathustra Amadeus Goertzel and Cezary Kaliszyk and Mirek Ols{\'{a}}k and Bartosz Piotrowski and Stephan Schulz and Martin Suda and Josef Urban}, editor = {Adam Naumowicz and Ren{\'{e}} Thiemann}, title = {{MizAR} 60 for {M}izar 50}, booktitle = {14th International Conference on Interactive Theorem Proving, {ITP} 2023}, series = {LIPIcs}, volume = {268}, pages = {19:1--19:22}, publisher = {Schloss Dagstuhl}, year = {2023}, url = {https://doi.org/10.4230/LIPIcs.ITP.2023.19}, doi = {10.4230/LIPICS.ITP.2023.19},}
- Details
- Category: Publications 2023
Christina Kohl, Aart Middeldorp
Proceedings of the 14th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics 268, pp. 38:1-38:8, 2023.
pdf doi:10.4230/LIPIcs.ITP.2023.38
Abstract
We report on the first formalization of the almost-development closedness criterion for confluence of left-linear term rewrite systems and illustrate a problem we encountered while trying to formalize the original paper proof by van Oostrom.
BibTex
@inproceedings{CKAM-ITP23, author = "Christina Kohl and Aart Middeldorp", title = "Formalizing Almost Development Closed Critical Pairs", booktitle = "Proceedings of the 14th International Conference on Interactive Theorem Proving", editor = "Adam Naumowicz and Ren\'e Thiemann", series = "Leibniz International Proceedings in Informatics", volume = 268, pages = "38:1--38:8", year = 2023, doi = "10.4230/LIPIcs.ITP.2023.38"}
- Details
- Category: Publications 2023
Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, René Thiemann, Akihisa Yamada
Abstract
We propose a new format for a variety of rewrite systems, to replace the current COPS format used in the Confluence Competition. We include a proposal for logically constrained rewrite system, to prepare for a future competition category.
BibTex
@inproceedings{AHKKMMNSSSTY-IWC23, author = "Takahito Aoto and Nao Hirokawa and Dohan Kim and Misaki Kojima and Aart Middeldorp and Fabian Mitterwallner and Naoki Nishida and Teppei Saito and Jonas Sch{\"o}pf and Kiraku Shintani and Ren{\'e} Thiemann and Akihisa Yamada", title = "A New Format for Rewrite Systems", booktitle = "Proceedings of the 12th International Workshop on Confluence", pages = "32--37", year = 2023}
- Details
- Category: Publications 2023
Jan Jakubův and Cezary Kaliszyk
Intelligent Computer Mathematics – 16th International Conference, CICM 2023, pp. 303-308, 2023.
pdf doi:10.1007/978-3-031-42753-4_22
Abstract
We present a system for the visualization of proofs originating from Automated Theorem Provers for first-order logic. The system can hide uninteresting proof parts of proofs, such as type annotations, translate first-order terms to standard math syntax, and compactly display complex formulas. We demonstrate the system on several non-trivial automated proofs of statements from Mizar Mathematical Library translated to first-order logic, and we provide a web interface where curious users can browse and investigate the proofs.
BibTex
@inproceedings{jjck-cicm23, author = {Jan Jakubuv and Cezary Kaliszyk}, editor = {Catherine Dubois and Manfred Kerber}, title = {{VizAR: V}isualization of Automated Reasoning Proofs (System Description)}, booktitle = {Intelligent Computer Mathematics - 16th International Conference, {CICM} 2023}, series = {LNCS}, volume = {14101}, pages = {303--308}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-42753-4\_22}, doi = {10.1007/978-3-031-42753-4\_22},}
- Details
- Category: Publications 2023
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 401-418, 2023
pdf doi:10.1007/978-3-031-38499-8_27
Abstract
We revisit AC completion for left-linear term rewrite systems where AC unification is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process. Finally, we present experimental results for our implementation of left-linear AC completion in the tool accompll.
BibTex
@inproceedings{JNNHAM-CADE23, author = "Johannes Niederhauser and Nao Hirokawa and Aart Middeldorp", title = "Left-Linear Completion with {AC} Axioms", booktitle = "Proceedings of the 29th International Conference on Automated Deduction", editor = "Brigitte Pientka and Cesare Tinelli", series = "Lecture Notes in Artificial Intelligence", volume = 14132, pages = "401--418", year = 2023, doi = "10.1007/978-3-031-38499-8\_23"}
- Details
- Category: Publications 2023
Jonas Schöpf, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 474-490, 2023.
pdf doi:10.1007/978-3-031-38499-8_27
Abstract
Numerous confluence criteria for plain term rewrite systems are known. For logically constrained rewrite system, an attractive extension of term rewriting in which rules are equipped with logical constraints, much less is known. In this paper we extend the strongly-closed and (almost) parallel-closed critical pair criteria of Huet and Toyama to the logically constrained setting. We discuss the challenges for automation and present crest, a new tool for logically constrained rewriting in which the confluence criteria are implemented, together with experimental data.
BibTex
@inproceedings{JSAM-CADE23, author = "Jonas Sch\"{o}pf and Aart Middeldorp", title = "Confluence Criteria for Logically Constrained Rewrite Systems", booktitle = "Proceedings of the 29th International Conference on Automated Deduction", editor = "Brigitte Pientka and Cesare Tinelli", series = "Lecture Notes in Artificial Intelligence", volume = 14132, pages = "474--490", year = 2023, doi = "10.1007/978-3-031-38499-8\_27"}
- Details
- Category: Publications 2023
Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
Frontiers of Combining Systems – 14th International Symposium, FroCoS 2023, pp. 236-254, 2023.
pdf doi:10.1007/978-3-031-43369-6_13 AFP entry
Abstract
Interactive theorem provers are today increasingly used to certify mathematical theories. To formally prove a theorem, reasoning procedures called tactics are invoked successively on the proof states starting with the initial theorem statement, transforming them into subsequent intermediate goals, and ultimately discharging all proof obligations. In this work, we develop and experimentally evaluate approaches that predict the most likely tactics that will achieve particular desired transformations of proof states. First, we design several characterizations to efficiently capture the semantics of the proof transformations. Then we use them to create large datasets on which we train state-of-the-art random forests and language models. The trained models are evaluated experimentally, and we show that our best model is able to guess the right tactic for a given proof transformation in 74% of the cases. Finally, we use the trained methods in two applications: proof shortening and tactic suggesting. To the best of our knowledge, this is the first time that tactic synthesis is trained on proof transformations and assists interactive theorem proving in these ways.
BibTex
@inproceedings{lzlbckju-frocos23, author = {Liao Zhang and Lasse Blaauwbroek and Cezary Kaliszyk and Josef Urban}, editor = {Uli Sattler and Martin Suda}, title = {Learning Proof Transformations and Its Applications in Interactive Theorem Proving}, booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023}, series = {LNCS}, volume = {14279}, pages = {236--254}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-43369-6\_13}, doi = {10.1007/978-3-031-43369-6\_13},}
- Details
- Category: Publications 2023
Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
The multiple-angle formulas for the sine and cosine functions state that for any natural number n, the values of cos(nx) and sin(nx) and can be expressed in terms cos(x) of and sin(x). To be more precise, there are polynomials T(n) and U(n) such that cos(nx) = T(n, cos(x)) and sin(nx) = U(n, cos(x)) sin(x). These are called the Chebyshev polynomials of the first and second kind, respectively.
This entry contains a definition of these two familes of polynomials in Isabelle/HOL along with some of their most important properties. In particular, it is shown that T(n) and U(n) are orthogonal families of polynomials. Moreover, we show the well-known result that monic polynomial of degree has a supremum norm of at least 2^(n-1) on the unit interval , and that this inequality is sharp since equality holds with p = 2^(1-n) T(n). This has important consequences in the theory of function interpolation, since it implies that the roots of T(n) (also colled the Chebyshev nodes) are exceptionally well-suited as interpolation nodes.
BibTex
@article{Chebyshev_Polynomials-AFP, author = {Manuel Eberl}, title = {Chebyshev Polynomials}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Chebyshev_Polynomials.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Manuel Eberl, Katharina Kreuzer
Archive of Formal Proofs 2023.
Abstract
This entry provides a type class for perfect fields. A perfect field K can be characterized by one of the following equivalent conditions:
1. Any irreducible polynomial p is separable, i.e. gcd(p,p’) = 1, or, equivalently, p’ is non-zero.
2. Either the characteristic of K is 0 or p > 0 and the Frobenius endomorphism is surjective (i.e. every element of K has a p-th root).
We define perfect fields using the second characterization and show the equivalence to the first characterization. The implication in one direction is relatively straightforward using the injectivity of the Frobenius homomorphism. Examples for perfect fields are:
1. any field of characteristic 0 (e.g. the reals or complex numbers), 2. any finite field, 3. any algebraically closed field.
BibTex
@article{Perfect_Fields-AFP, author = {Manuel Eberl and Katharina Kreuzer}, title = {Perfect Fields}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Perfect_Fields.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Katharina Kreuzer, Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
This article formalises the Elimination of Repeated Factors (ERF) Algorithm. This is an algorithm to find the square-free part of polynomials over perfect fields. Notably, this encompasses all fields of characteristic 0 and all finite fields. For fields with characteristic 0, the ERF algorithm proceeds similarly to the classical Yun algorithm. However, for fields with non-zero characteristic p, Yun’s algorithm can fail because the derivative of a non-zero polynomial can be 0. The ERF algorithm detects this case and therefore also works in this more general setting. To state the ERF Algorithm in this general form, we build on the entry on perfect fields. We show that the ERF algorithm is correct and returns a list of pairwise coprime square-free polynomials whose product is the input polynomial. Indeed, through this, the ERF algorithm also yields executable code for calculating the square-free part of a polynomial (denoted by the function radical).
BibTex
@article{Elimination_Of_Repeated_Factors-AFP, author = {Katharina Kreuzer and Manuel Eberl}, title = {Elimination of Repeated Factors Algorithm}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Elimination_Of_Repeated_Factors.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
This entry formalises two well-known results about the geometric relation between the roots of a complex polynomial and its critical points, i.e. the roots of its derivative. The first of these is the Gauß–Lucas Theorem: The critical points of a complex polynomial lie inside the convex hull of its roots. The second one is Jensen’s Theorem: Every non-real critical point of a real polynomial lies inside a disc between two conjugate roots. These discs are called the Jensen discs: the Jensen disc of a pair of conjugate roots a ± bi is the smallest disc that contains both of them, i.e. the disc with centre a and radius b.
BibTex
@article{Polynomial_Crit_Geometry-AFP, author = {Manuel Eberl}, title = {Two theorems about the geometry of the critical points of a complex polynomial}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Polynomial_Crit_Geometry.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
This entry provides a formalisation of Lambert series, i.e. series of the form ∑a(n) q^n/(1-q^n), where a(n) is a sequence of real or complex numbers. Proofs for all the basic properties are provided, such as: the precise region in which the series converges, the functional equation it satisfies under the map f(q) = 1/q, the power series expansion at q = 0, expressing a Lambert series in terms of the associated ‘normal’ power series, and connections to various number-theoretic functions like the divisor σ function. The formalisation mainly follows the chapter on Lambert series in Konrad Knopp’s classic textbook Theory and Application of Infinite Series and includes all results presented therein.
BibTex
@article{Lambert_Series-AFP, author = {Manuel Eberl}, title = {Lambert Series}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Lambert_Series.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
This entry provides a definition of the Polylogarithm function, commonly denoted as Li(a,z). Here, z is a complex number and a an integer parameter. This function can be defined by a power series for |z| < 1 and analytically extended to the entire complex plane, except for a branch cut on the reals ≥ 1. Several basic properties are also proven, such as the relationship to the Eulerian polynomials, the derivative formula, the relationship to the ‘normal’ logarithm, and the duplication formula.
BibTex
@article{Polylog-AFP, author = {Manuel Eberl}, title = {The Polylogarithm Function}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Polylog.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023
Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
This entry presents a short derivation of the cardinality of the real numbers, namely that it is the same as the cardinality of the power set of the naturals. This is done by giving an injection in both directions: in the one direction via Dedekind cuts, in the other direction via ternary fractions.
BibTex
@article{Cardinality_Continuum-AFP, author = {Manuel Eberl}, title = {The Cardinality of the Continuum}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Cardinality_Continuum.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2023