Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 132 – 143, 2019.
pdf 
doi:10.1145/3293880.3294098
Abstract
It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RRn relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.
BibTex
@inproceedings{BFAMPRFR-CPP19, author = "Bertram Felgenhauer and Aart Middeldorp and T.V.H. Prathamesh and Franziska Rapp", title = "A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in {Isabelle/HOL}", booktitle = "Proceedings of the 8th International {ACM SIGPLAN} International Conference on Certified Programs and Proofs", pages = "132--143", publisher = "ACM", doi = "10.1145/3293880.3294098", year = 2019}
- Details
- Category: Publications 2019
Alexander Lochmann, Christian Sternagel
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 144 – 151, 2019.
pdf doi:10.1145/3293880.3294099
Abstract
Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding AC-rules to a rewrite system, we switch to the notion of AC-termination. AC-termination can for example be shown using AC-compatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an AC-compatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of AC-termination proofs generated by automated termination tools.
BibTex
@inproceedings{ALCS-CPP19, author = "Alexander Lochmann and Christian Sternagel", title = "Certified {ACKBO}", booktitle = "Proceedings of the 8th International Conference on Certified Programs and Proofs", editor = "Assia Mahboubi and Magnus O. Myreen", pages = "144--151", year = 2019, doi = "10.1145/3293880.3294099"}
- Details
- Category: Publications 2019
Ralph Bottesch, Max W. Haslbeck, René Thiemann
Archive of Formal Proofs 2019.
Abstract
We formalize a proof of Motzkin’s transposition theorem and Farkas’ lemma in Isabelle/HOL. Our proof is based on the formalization of the simplex algorithm which, given a set of linear constraints, either returns a satisfying assignment to the problem or detects unsatisfiability. By reusing facts about the simplex algorithm we show that a set of linear constraints is unsatisfiable if and only if there is a linear combination of the constraints which evaluates to a trivially unsatisfiable inequality.
BibTex
@article{Farkas-AFP, author = {Ralph Bottesch and Max W. Haslbeck and René Thiemann}, title = {Farkas' Lemma and Motzkin's Transposition Theorem}, journal = {Archive of Formal Proofs}, month = jan, year = 2019, note = {\url{https://isa-afp.org/entries/Farkas.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2019
Jouke Witteveen, Ralph Bottesch, Leen Torenvliet
45th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2019), Lecture Notes in Computer Science 11376, pp. 504 – 518, 2019.
pdf doi:10.1007/978-3-030-10801-4
Springer Nature Switzerland AG 2019
Abstract
In parameterized algorithmics, the process of kernelization is defined as a polynomial time algorithm that transforms the instance of a given problem to an equivalent instance of a size that is limited by a function of the parameter. As, afterwards, this smaller instance can then be solved to find an answer to the original question, kernelization is often presented as a form of preprocessing. A natural generalization of kernelization is the process that allows for a number of smaller instances to be produced to provide an answer to the original problem, possibly also using negation. This generalization is called Turing kernelization. Immediately, questions of equivalence occur or, when is one form possible and not the other. These have been long standing open problems in parameterized complexity. In the present paper, we answer many of these. In particular, we show that Turing kernelizations differ not only from regular kernelization, but also from intermediate forms as truth-table kernelizations. We achieve absolute results by diagonalizations and also results on natural problems depending on widely accepted complexity theoretic assumptions. In particular, we improve on known lower bounds for the kernel size of compositional problems using these assumptions.
BibTex
@inproceedings{JWRBLT-SOFSEM19, author = "Jouke Witteveen and Ralph Bottesch and Leen Torenvliet", title = "A Hierarchy of Polynomial Kernels", booktitle = "Proceedings of the 45th International Conference on Current Trends in Theory and Practice of Computer Science", series = "Lecture Notes in Computer Science", volume = 11376, pages = "504--518", year = 2019, doi = "10.1007/978-3-030-10801-4"}
- Details
- Category: Publications 2019
Aart Middeldorp, Julian Nagele, and Kiraku Shintani
Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019, part III), Lecture Notes in Computer Science 11429, pp. 25 – 40, 2019.
pdf doi:10.1007/978-3-030-17502-3_2
Abstract
We report on the 2019 edition of the Confluence Competition, a competition of software tools that aim to prove or disprove confluence and related (undecidable) properties of rewrite systems automatically.
BibTex
@inproceedings{MNS-TACAS19, author = "Aart Middeldorp and Julian Nagele and Kiraku Shintani", title = "Confluence Competition 2019", booktitle = "Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Part III)", editor = "Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen", series = "Lecture Notes in Computer Science", volume = 11429, pages = "25--40", year = 2019, doi = "10.1007/978-3-030-17502-3_2"}
- Details
- Category: Publications 2019
Florian Meßner, Christian Sternagel
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11427, pp. 337 – 343, 2019.
pdf doi:10.1007/978-3-030-17462-0_19
Abstract
We introduce nonreach, an automated tool for nonreachability analysis that is intended as a drop-in addition to existing termination and confluence tools for term rewriting. Our preliminary experimental data suggests that nonreach can improve the performance of existing termination tools.
BibTex
@inproceedings{FMCS-TACAS19, author = "Florian Meßner and Christian Sternagel", title = "nonreach -- {A} Tool for Nonreachability Analysis", booktitle = "Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Tomáš Vojnar and Lijun Zhang", series = "Lecture Notes in Computer Science", volume = 11427, pages = "337--343", year = 2019, doi = "10.1007/978-3-030-17462-0_19"}
- Details
- Category: Publications 2019
Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11429, pp. 155 – 166, 2019.
pdf doi:10.1007/978-3-030-17462-0_15
Abstract
The termination and complexity competition (termCOMP) focuses on automated termination and complexity analysis for various
kinds of programming paradigms, including categories for term rewriting, integer transition systems, imperative programming, logic programming, and functional programming. In all categories, the competition also welcomes the participation of tools providing certifiable output. The goal of the competition is to demonstrate the power and advances of the state-of-the-art tools in each of these areas.
BibTex
@inproceedings{CSAY-TACAS19, author = "Christian Sternagel and Akihisa Yamada", title = "Reachability Analysis for Termination and Confluence of Rewriting", booktitle = "Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Tomáš Vojnar and Lijun Zhang", series = "Lecture Notes in Computer Science", volume = 11427, pages = "262--278", year = 2019, doi = "10.1007/978-3-030-17462-0_15"}
- Details
- Category: Publications 2019
Christian Sternagel, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11427, pp. 262 – 278, 2019.
pdf doi:10.1007/978-3-030-17462-0_15
Abstract
In term rewriting, reachability analysis is concerned with the problem of deciding whether or not one term is reachable from another by rewriting. Reachability analysis has several applications in termination and confluence analysis of rewrite systems. We give a unified view on reachability analysis for rewriting with and without conditions by means of what we call reachability constraints. Moreover, we provide several techniques that fit into this general framework and can be efficiently implemented. Our experiments show that these techniques increase the power of existing termination and confluence tools.
BibTex
@inproceedings{CSAY-TACAS19, author = "Christian Sternagel and Akihisa Yamada", title = "Reachability Analysis for Termination and Confluence of Rewriting", booktitle = "Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Tomáš Vojnar and Lijun Zhang", series = "Lecture Notes in Computer Science", volume = 11427, pages = "262--278", year = 2019, doi = "10.1007/978-3-030-17462-0_15"}
- Details
- Category: Publications 2019
Bartosz Piotrowski, Josef Urban, Chad Brown, Cezary Kaliszyk
Learning and Reasoning with Graph-Structured Representations, ICML 2019 Workshop, 2019.
pdf doi:10.1007/s10817-019-09526-y
Abstract
This work investigates if the current neural architectures are adequate for learning symbolic rewriting. Two kinds of data sets are proposed for this research – one based on automated proofs and the other being a synthetic set of polynomial terms. The experiments with use of the current neural machine translation models are performed and its results are discussed. Ideas for extending this line of research are proposed and its relevance is motivated.
BibTex
@incollection{bpjucbck-lrgsr19, title = {Can Neural Networks Learn Symbolic Rewriting?}, author = {Bartosz Piotrowski and Josef Urban and Chad Brown and Cezary Kaliszyk}, booktitle = {Learning and Reasoning with Graph-Structured Representations -- ICML 2019 Workshop}, pages = {1--4}, year = {2019}, url = {https://graphreason.github.io/papers/40.pdf}}
- Details
- Category: Publications 2019
Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada
Journal of Automated Reasoning 64(4), pp. 699 – 735, 2020.
pdf doi:10.1007/s10817-019-09526-y
Abstract
We formally verify 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 factorization in the prime field GF(p) and then performs computations in the ring of integers 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 locales and local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds.
BibTex
@article{JDSJRTAY-JAR19, author = "Jose Divas\'on and Sebastiaan Joosten and Ren\'e Thiemann and Akihisa Yamada", title = "A Verified Implementation of the {B}erlekamp--{Z}assenhaus Factorization Algorithm", journal = "Journal of Automated Reasoning", volume = 64, number = 4, year = 2020, pages = "699--735", doi = "10.1007/s10817-019-09526-y", note = "Online first."}
- Details
- Category: Publications 2019
Ralph Bottesch, Max W. Haslbeck, and René Thiemann
International Symposium on Frontiers of Combining Systems, Lecture Notes in Computer Science 11715, pp. 223 – 239, 2019.
pdf doi:10.1007/978-3-030-29007-8_13
Abstract
Dutertre and de Moura developed a simplex-based solver for linear rational arithmetic that has an incremental interface and provides unsatisfiable cores. We present a verification of their algorithm in Isabelle/HOL that significantly extends previous work by Spasić and Marić. Based on the simplex algorithm we further formalize Farkas’ Lemma. With this result we verify that linear rational constraints are satisfiable over Q if and only they are satisfiable over R. Hence, our verified simplex algorithm is also able to decide satisfiability in linear real arithmetic.
BibTex
@inproceedings{RBMHRT-FROCOS19, author = "Ralph Bottesch and Max W. Haslbeck and René Thiemann", title = "Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL", booktitle = "Proceedings of the 12th International Symposium on Frontiers of Combining Systems", editor = "A. Herzig and A. Popescu", series = "Lecture Notes in Computer Science", volume = 11715, pages = "223--239", year = 2019, doi = "10.1007/978-3-030-29007-8_13"}
- Details
- Category: Publications 2019
Christina Kohl and Aart Middeldorp
27th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 11716, pp. 337 – 353, 2019.
pdf doi:10.1007/978-3-030-29436-6_20
Abstract
Proof terms are a useful concept for comparing computations in term rewriting. We analyze proof terms with composition, with an eye towards automation. We revisit permutation equivalence and projection equivalence, two key notions presented in the literature. We report on the integration of proof terms with composition into ProTeM, a tool for manipulating proof terms.
BibTex
@inproceedings{CKAM-CADE19, author = "Christina Kohl and Aart Middeldorp", title = "Composing Proof Terms", booktitle = "Proceedings of the 27th International Conference on Automated Deduction", editor = "Pascal Fontaine", series = "Lecture Notes in Artificial Intelligence", volume = 11716, pages = "337--353", year = 2019, doi = "10.1007/978-3-030-29436-6_20"}
- Details
- Category: Publications 2019
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
6th Workshop on Proof eXchange for Theorem Proving, EPTCS 301, pp. 18 – 26, 2019.
Abstract
This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver CVC4. While many of these were proved in a completely automatic fashion for any bit-width, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over arbitrary bit-widths. In this paper we describe our initial efforts in proving a subset of these invertibility conditions in the Coq proof assistant. We describe the Coq library that we use, as well as the extensions that we introduced to it.
BibTex
@inproceedings{beavyzcbct-pxtp19, author = {Burak Ekici and Arjun Viswanathan and Yoni Zohar and Clark W. Barrett and Cesare Tinelli}, title = {Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)}, booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, pages = {18--26}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301.4}, doi = {10.4204/EPTCS.301.4}, editor = {Giselle Reis and Haniel Barbosa}, series = {{EPTCS}}, volume = {301},}
- Details
- Category: Publications 2019
Ralph Bottesch, Alban Reynaud, René Thiemann
Archive of Formal Proofs 2019.
Abstract
We formalize results about linear inqualities, mainly from Schrijver’s book. The main results are the proof of the fundamental theorem on linear inequalities, Farkas’ lemma, Carathéodory’s theorem, the Farkas-Minkowsky-Weyl theorem, the decomposition theorem of polyhedra, and Meyer’s result that the integer hull of a polyhedron is a polyhedron itself. Several theorems include bounds on the appearing numbers, and in particular we provide an a-priori bound on mixed-integer solutions of linear inequalities.
BibTex
@article{Linear_Inequalities-AFP, author = {Ralph Bottesch and Alban Reynaud and René Thiemann}, title = {Linear Inequalities}, journal = {Archive of Formal Proofs}, month = jun, year = 2019, note = {\url{http://isa-afp.org/entries/Linear_Inequalities.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2019
Chad Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
27th International Conference on Automated Deduction, LNCS 11716, pp. 123 – 141, 2019.
pdf doi:10.1007/978-3-030-29436-6_8
Abstract
This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.
BibTex
@inproceedings{cbtgckgsju-cade19, author = {Chad Brown and Thibault Gauthier and Cezary Kaliszyk and Geoff Sutcliffe and Josef Urban}, title = {{GRUNGE:} {A} Grand Unified {ATP} Challenge}, booktitle = {The 27th International Conference on Automated Deduction (CADE 2019)}, year = {2019}, series = {LNCS}, pages = {123--141}, editor = {Pascal Fontaine}, volume = {11716}, publisher = {Springer}, url = {https://doi.org/10.1007/978-3-030-29436-6_8}, doi = {10.1007/978-3-030-29436-6_8},}
- Details
- Category: Publications 2019
Christian Sternagel and Sarah Winkler
27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 508 – 525, 2019.
pdf doi:10.1007/978-3-030-29436-6_30
Creative Commons License – CC BY 4.0
Abstract
On the one hand, equational reasoning is a fundamental part of automated theorem proving with ordered completion as a key technique. On the other hand, the complexity of corresponding, often highly optimized, automated reasoning tools makes implementations inherently error-prone. As a remedy, we provide a formally verified certifier for ordered completion based techniques. This certifier is code generated from an accompanying Isabelle/HOL formalization of ordered rewriting and ordered completion incorporating an advanced ground joinability criterion. It allows us to rigorously validate generated proof certificates from several domains: ordered completion, satisfiability in equational logic, and confluence of conditional term rewriting.
BibTex
@inproceedings{CSSW-CADE19, author = "Christian Sternagel and Sarah Winkler", title = "Certified Equational Reasoning via Ordered Completion", booktitle = "Proceedings of the 27th International Conference on Automated Deduction", editor = "Pascal Fontaine", series = "Lecture Notes in Computer Science", volume = 11716, pages = "508--525", year = 2019, doi = "10.1007/978-3-030-29436-6_30"}
- Details
- Category: Publications 2019
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Logical Methods in Computer Science, 15(3), pp. 19:1 – 19:42, 2019.
pdf doi:10.23638/LMCS-15(3:19)2019
Creative Commons License – CC BY 4.0
Abstract
Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.
BibTex
@article{HMSW-LMCS19, author = "Nao Hirokawa and Aart Middeldorp and Christian Sternagel and Sarah Winkler", title = "Abstract Completion, Formalized", journal = "Logical Methods in Computer Science", volume = 15, number = 3, pages = "19:1--19:42", year = 2019, doi = "10.23638/LMCS-15(3:19)2019"}
- Details
- Category: Publications 2019
Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi
27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 319 – 336, 2019.
pdf doi:10.1007/978-3-030-29436-6_19
Springer Nature Switzerland AG 2019
Abstract
We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating.
BibTex
@inproceedings{NHJNVvOMO-CADE27, author = "Nao Hirokawa and Julian Nagele and Vincent van Oostrom and Michio Oyamaguchi", title = "Confluence by Critical Pair Analysis Revisited", booktitle = "Proceedings of the 27th International Conference on Automated Deduction", editor = "Pascal Fontaine", series = "Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence", volume = 11716, pages = "319-336", year = 2019, publisher = "Springer", doi = "https://doi.org/10.1007/978-3-030-29436-6_19" arxiv = "https://arxiv.org/abs/1905.11733v2"}
- Details
- Category: Publications 2019
Michael Färber, Cezary Kaliszyk
28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, LNCS 11714, pp. 21 – 38, 2019.
pdf doi:10.1007/978-3-030-29026-9_2
Abstract
Nonclausal connection tableaux calculi enable proof search without performing clausification. We give a translation of nonclausal connection proofs to Gentzen’s sequent calculus LK and compare it to an existing translation of clausal connection proofs. Furthermore, we implement the translation in the interactive theorem prover HOL Light, enabling certification of nonclausal connection proofs as well as a new, complementary automation technique in HOL Light.
BibTex
@inproceedings{mfck-tableaux19, author = {Michael Färber and Cezary Kaliszyk}, title = {Certification of Nonclausal Connection Tableaux Proofs}, booktitle = {28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019)}, year = {2019}, series = {LNCS}, pages = {21--38}, url = {https://doi.org/10.1007/978-3-030-29026-9_2}, doi = {10.1007/978-3-030-29026-9_2}, publisher = {Springer}, volume = {11714}, editor = {Serenella Cerrito and Andrei Popescu},}
- Details
- Category: Publications 2019
Cezary Kaliszyk, Karol Pąk
10th International Conference on Interactive Theorem Proving, LIPIcs 141, pp. 35:1 – 35:7, 2019.
pdf doi:10.4230/LIPIcs.ITP.2019.35
Abstract
Declarative proof styles of different proof assistants include a number of incompatible features. In this paper we discuss and classify the differences between them and propose efficient algorithms for declarative proof outline translation. We demonstrate the practicality of out algorithms by automatically translating the proof outlines in 200 articles from the Mizar Mathematical Library to the Isabelle/Isar proof style. This generates the corresponding theories with 15301 proof outlines accepted by the Isabelle proof checker. The goal of our translation is to produce a declarative proof in the target system that is both accepted and short and therefore readable. For this three kinds of adaptations are required. First, the proof structure often needs to be rebuilt to capture the extensions of the natural deduction rules supported by the systems. Second, the references to previous items and their labels need to be matched and aligned. Finally, adaptations in the annotations of individual proof step may be necessary.
BibTex
@inproceedings{ckkp-itp19, author = {Cezary Kaliszyk and Karol Pąk}, title = {Declarative Proof Translation (short paper)}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, year = {2019}, series = {LIPIcs}, pages = {35:1--35:7}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.35}, doi = {10.4230/LIPIcs.ITP.2019.35}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, volume = {141},}
- Details
- Category: Publications 2019
Chad Brown, Cezary Kaliszyk, Karol Pąk
10th International Conference on Interactive Theorem Proving, LIPIcs 141, pp. 9:1 – 9:16, 2019.
pdf doi:10.4230/LIPIcs.ITP.2019.9
Abstract
We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange’s four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework.
BibTex
@inproceedings{cbckkp-itp19, author = {Chad Brown and Cezary Kaliszyk and Karol Pąk}, title = {Higher-order {T}arski {G}rothendieck as a Foundation for Formal Proof}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, year = {2019}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, pages = {9:1--9:16}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.9}, doi = {10.4230/LIPIcs.ITP.2019.9}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, volume = {141},}
- Details
- Category: Publications 2019