Jose Divason, Sebastiaan J. C. Joosten, Rene Thiemann and Akihisa Yamada
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), pp. 17 – 29, 2017.
pdf 
doi:10.1145/3018610.3018617
Abstract
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 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 Isabelle’s recent addition of local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.
BibTex
@inproceedings{JoostenCPP2017, author = {Jos{\'{e}} Divas{\'{o}}n and Sebastiaan J. C. Joosten and Ren{\'{e}} Thiemann and Akihisa Yamada}, title = {A Formalization of the {B}erlekamp--{Z}assenhaus Factorization Algorithm}, booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}, series = {CPP 2017}, year = {2017}, isbn = {978-1-4503-4705-1}, location = {Paris, France}, pages = {17--29}, numpages = {13}, url = {http://doi.acm.org/10.1145/3018610.3018617}, doi = {10.1145/3018610.3018617}, acmid = {3018617}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Isabelle, Polynomial Factorization, Prime Fields}}
- Details
- Category: Publications 2017
Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann
Journal of Automated Reasoning, 58(1), pp. 3 – 31, 2017.
pdf doi:10.1007/s10817-016-9388-y
Abstract
In this system description, we present the tool AProVE for automatic termination and complexity proofs of Java, C, Haskell, Prolog, and rewrite systems. In addition to classical term rewrite systems (TRSs), AProVE also supports rewrite systems containing built-in integers (int-TRSs). To analyze programs in high-level languages, AProVE automatically converts them to (int-)TRSs. Then, a wide range of techniques is employed to prove termination and to infer complexity bounds for the resulting rewrite systems. The generated proofs can be exported to check their correctness using automatic certifiers. To use AProVE in software construction, we present a corresponding plug-in for the popular Eclipse software development environment.
BibTex
@article{AProVE-JAR17, author = {J{\"{u}}rgen Giesl and Cornelius Aschermann and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Jera Hensel and Carsten Otto and Martin Pl{\"{u}}cker and Peter Schneider{-}Kamp and Thomas Str{\"{o}}der and Stephanie Swiderski and Ren{\'{e}} Thiemann}, title = {Analyzing Program Termination and Complexity Automatically with {AProVE}}, journal = {Journal of Automated Reasoning}, volume = {58}, number = {1}, pages = {3--31}, year = {2017}, doi = {10.1007/s10817-016-9388-y},}
- Details
- Category: Publications 2017
Cynthia Kop, Aart Middeldorp, Thomas Sternagel
Logical Methods in Computer Science 13(1:6), pp. 1 – 56, 2017.
pdf doi:10.23638/LMCS-13(1:6)2017
Creative Commons License
Abstract
We propose a notion of complexity for oriented conditional rewrite systems satisfying certain restrictions. This notion is realistic in the sense that it measures not only successful computations, but also partial computations that result in a failed rule application. A transformation to unconditional context-sensitive rewrite systems is presented which reflects this complexity notion, as well as a technique to derive runtime and derivational complexity bounds for the result of this transformation.
BibTex
@article{CKAMTS-LMCS17, author = "Cynthia Kop and Aart Middeldorp and Thomas Sternagel", title = "Complexity of Conditional Term Rewriting", journal = "Logical Methods in Computer Science", volume = 13, issue = "1:6", pages = "1--56", year = 2017, doi = "10.23638/LMCS-13(1:6)2017"}
- Details
- Category: Publications 2017
José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
Journal of Automated Reasoning 58(3), pp. 391 – 411, 2017.
pdf doi:10.1007/s10817-016-9373-5
Abstract
A term rewrite system is terminating when no infinite reduction sequences arepossible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.
BibTex
@article{INVY-JAR2017, author = "Jos{\'e} Iborra and Naoki Nishida and Germ{\'a}n Vidal and Akihisa Yamada", title = "Relative Termination via Dependency Pairs", journal = "Journal of Automated Reasoning", year = 2017, volume = 58, number = 3, pages = "391-411", doi = "10.1007/s10817-016-9373-5"}
- Details
- Category: Publications 2017
David Aspinall, Cezary Kaliszyk
19th International Conference on Fundamental Approaches to Software Engineering, LNCS 9633, pp. 325-341, 2016.
pdf doi:10.1007/978-3-662-49665-7_19
Abstract
Recent years have seen increasing success in building large formal proof developments using interactive theorem provers (ITPs). Some proofs have involved many authors, years of effort, and resulted in large, complex interdependent sets of proof “source code” files. Developing these in the first place, and maintaining and extending them afterwards, is a considerable challenge. It has prompted the idea of Proof Engineering as a new sub-field, to find methods and tools to help. It is natural to try to borrow ideas from Software Engineering for this.
In this paper we investigate the idea of defining proof metrics by analogy with software metrics. We seek metrics that may help to monitor and compare formal proof developments, which might be used to guide good practice, locate likely problem areas, or suggest refactorings. Starting from metrics that have been proposed for object-oriented design, we define analogues for formal proofs. We show that our metrics enjoy reasonable properties, and we demonstrate their behaviour with some practical experiments, showing changes over time as proof developments evolve, and making comparisons across between different ITPs.
BibTex
@inproceedings{dack-fase16, author = {David Aspinall and Cezary Kaliszyk}, title = {Towards Formal Proof Metrics}, booktitle = {19th International Conference on Fundamental Approachesto Software Engineering (FASE 2016)}, pages = {325--341}, year = {2016}, editor = {Perdita Stevens and Andrzej Wasowski}, series = {Lecture Notes in Computer Science}, volume = {9633}, publisher = {Springer}, doi = {10.1007/978-3-662-49665-7_19},}
- Details
- Category: Publications 2017
Bertram Felgenhauer and René Thiemann
Information and Computation 253(3), pp. 467 – 483, 2017
pdf doi:10.1016/j.ic.2016.06.011
Abstract
Regular tree languages are a popular device for reachability analysis over term rewrite systems, with many applications like analysis of cryptographic protocols, or confluence and termination analysis. At the heart of this approach lies tree automata completion, first introduced by Genet for left-linear rewrite systems. Korp and Middeldorp introduced so-called quasi-deterministic automata to extend the technique to non-left-linear systems. In this paper, we introduce the simpler notion of state-compatible automata, which are slightly more general than quasi-deterministic, compatible automata. This notion also allows us to decide whether a regular tree language is closed under rewriting, a problem which was not known to be decidable before.
The improved precision has a positive impact in applications which are based on reachability analysis, namely termination and confluence analysis.
Our results have been formalized in the theorem prover Isabelle/HOL. This allows to certify automatically generated proofs that are using tree automata techniques.
BibTex
@article{FT-IC17, author = "Bertram Felgenhauer and Ren\'e Thiemann", title = "Reachability, Confluence, and Termination Analysis with State-Compatible Automata", journal = "Information and Computation", volume = 253, number = 3, pages = "467--483", year = 2017, doi = "10.1016/j.ic.2016.06.011"}
- Details
- Category: Publications 2017
Sebastiaan Joosten and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2017.
Abstract
We formalize the theory of subresultants and the subresultant polynomial remainder sequence as described by Brown and Traub. As a result, we obtain efficient certified algorithms for computing the resultant and the greatest common divisor of polynomials.
BibTex
@inproceedings{JoostenCPP2017, author = {Jos{\'{e}} Divas{\'{o}}n and Sebastiaan J. C. Joosten and Ren{\'{e}} Thiemann and Akihisa Yamada}, title = {A Formalization of the {B}erlekamp--{Z}assenhaus Factorization Algorithm}, booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}, series = {CPP 2017}, year = {2017}, isbn = {978-1-4503-4705-1}, location = {Paris, France}, pages = {17--29}, numpages = {13}, url = {http://doi.acm.org/10.1145/3018610.3018617}, doi = {10.1145/3018610.3018617}, acmid = {3018617}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Isabelle, Polynomial Factorization, Prime Fields}}
- Details
- Category: Publications 2017
Cezary Kaliszy, Josef Urban
Post proceedings of Semantic Web Collaborative Spaces, LNCS pp. 35-52, 2016.
pdf doi:10.1007/978-3-319-32667-2_3
Abstract
In the recent years, there have been significant advances in formalization of mathematics, involving a number of large-scale formalization projects. This naturally poses a number of interesting problems concerning how should humans and machines collaborate on such deeply semantic and computer-assisted projects. In this paper we provide an overview of the wikis and web-based systems for such collaboration involving humans and also AI systems over the large
corpora of fully formal mathematical knowledge.
BibTex
@inproceedings{ckju-swcs16, author = {Cezary Kaliszyk and Josef Urban}, title = {Wikis and Collaborative Systems for Large Formal Mathematics}, booktitle = {Semantic Web Collaborative Spaces}, pages = {35--52}, doi = {10.1007/978-3-319-32667-2_3}, editor = {Pascal Molli and John G. Breslin and Maria{-}Esther Vidal}, series = {LNCS}, volume = {9507}, publisher = {Springer}, year = {2016},}
- Details
- Category: Publications 2017
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPIC 46, pp. 125-143, 2017.
Abstract
Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such “hammer” techniques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences combined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39% of 7902 HOL4 theorems in 5 seconds whereas the best single HOLHammer strategy solves 32% in the same amount of time.
BibTex
@inproceedings{tgckju-lpar17, author = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban}, title = {{TacticToe}: Learning to Reason with {HOL4} Tactics}, booktitle = {LPAR-21. 21st International Conference on Logic forProgramming, Artificial Intelligence and Reasoning}, editor = {Thomas Eiter and David Sands}, series = {EPiC Series in Computing}, volume = {46}, pages = {125--143}, year = {2017}, publisher = {EasyChair}, bibsource = {EasyChair, http://www.easychair.org}, issn = {2398-7340}}
- Details
- Category: Publications 2017
Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk.
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC 46, pp. 85-105, 2017.
Abstract
Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go. Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification. Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved. Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.
BibTex
@inproceedings{slgicsck-lpar17, author = {Sarah Loos and Geoffrey Irving and Christian Szegedyand Cezary Kaliszyk}, title = {Deep Network Guided Proof Search}, booktitle = {LPAR-21. 21st International Conference on Logic forProgramming, Artificial Intelligence and Reasoning}, editor = {Thomas Eiter and David Sands}, series = {EPiC Series in Computing}, volume = {46}, pages = {85--105}, year = {2017}, publisher = {EasyChair}, bibsource = {EasyChair, http://www.easychair.org}, issn = {2398-7340}}
- Details
- Category: Publications 2017
Julian Nagele, Bertram Felgenhauer, and Harald Zankl
Logical Methods in Computer Science, 13(2:4), pp. 1 – 27, 2017.
pdf doi:10.23638/LMCS-13(2:4)2017
Abstract
The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.
BibTex
@article{NFZ-LMCS17, author = "Julian Nagele and Bertram Felgenhauer and Harald Zankl", title = "Certifying Confluence Proofs via Relative Termination and Rule Labeling", journal = "Logical Methods in Computer Science", volume = 13, number = "2:4", pages = "1--27", year = 2017, doi = "10.23638/LMCS-13(2:4)2017"}
- Details
- Category: Publications 2017
Sebastiaan J. C. Joosten
Relational and Algebraic Methods in Computer Science. RAMICS 2017, Lecture Notes in Computer Science 10226, pp. 159 – 176, 2017.
doi:10.1007/978-3-319-57418-9_10
Abstract
We introduce the tool Amperspiegel, which uses triple graphs for parsing, printing and manipulating data. We show how to conveniently encode parsers, graph manipulation-rules, and printers using several relations. As such, parsers, rules and printers are all encoded as graphs themselves. This allows us to parse, manipulate and print these parsers, rules and printers within the system. A parser for a context free grammar is graph-encoded with only four relations. The graph manipulation-rules turn out to be especially helpful when parsing. The printers strongly correspond to the parsers, being described using only five relations. The combination of parsers, rules and printers allows us to extract Ampersand source code from ArchiMate XML documents. Amperspiegel was originally developed to aid in the development of Ampersand.
BibTex
@inbook{Joosten2017, Address = {Cham}, Author = {Joosten, Sebastiaan J. C.}, Booktitle = {Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings}, Doi = {10.1007/978-3-319-57418-9_10}, Editor = {H{\"o}fner, Peter and Pous, Damien and Struth, Georg}, Isbn = {978-3-319-57418-9}, Pages = {159--176}, Publisher = {Springer International Publishing}, Title = {Parsing and Printing of and with Triples}, Url = {http://dx.doi.org/10.1007/978-3-319-57418-9_10}, Year = {2017}}
- Details
- Category: Publications 2017
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, Roland Zumkeller
Forum of Mathematics, Pi, 5, pp. 1-29, 2017.
Abstract
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
BibTex
@article{thetal-pi17, title={A Formal Proof of the {K}epler conjecture}, volume={5}, doi={10.1017/fmp.2017.1}, journal={Forum of Mathematics, Pi}, publisher={Cambridge University Press}, author={ Thomas Hales and Mark Adams and Gertrud Bauer and Tat Dat Dang and John Harrison and Le Truong Hoang and Cezary Kaliszyk and Victor Magron and Sean McLaughlin and Tat Thang Nguyen and Quang Truong Nguyen and Tobias Nipkow and Steven Obua and Joseph Pleso and Jason Rute and Alexey Solovyev and Thi Hoai Aa Ta and Nam Trung Tran and Thi Diep Trieu and Josef Urban and Ky Vu and Roland Zumkeller}, year={2017}}
- Details
- Category: Publications 2017
Carsten Fuhs, Cynthia Kop, Naoki Nishida
ACM Transactions on Computational Logic 18(2), pp. 14:1 – 14:50, 2017.
Abstract
This article aims to develop a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend transformation methods based on integer term rewriting systems to handle arbitrary data types, global variables, function calls, and arrays, and to encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations; thus, in contrast to other works, we do not require an explicit specification in a separate specification language.
BibTex
@article{CFCKNN-ACMTOCL17, author = "Carsten Fuhs and Cynthia Kop and Naoki Nishida", title = "Verifying Procedural Programs via Constrained Rewriting Induction", journal = "{ACM} Transactions on Computational Logic", volume = "18", issue = "2", pages = "14:1--14:50", year = 2017, doi = "10.1145/3060143"}
- Details
- Category: Publications 2017
Cezary Kaliszyk and Karol Pąk
10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 193-207, 2017.
pdf doi:10.1007/978-3-319-62075-6_14
Abstract
One of the crucial factors enabling an efficient use of a logical framework is the convenience of entering, manipulating, and presenting object logic constants, statements, and proofs. In this paper, we discuss various elements of the Mizar language and the possible ways how these can be represented in the Isabelle framework in order to allow a suitable way of working in typed set theory. We explain the interpretation of various components declared in each Mizar article environment and create Isabelle attributes and outer syntax that allow simulating them. We further discuss introducing notations for symbols defined in the Mizar Mathematical Library, but also synonyms and redefinitions of such symbols. We also compare the language elements corresponding to the actual proofs, with special care for implicit proof expansions not present in Isabelle. We finally discuss Mizar’s hidden arguments and demonstrate that some of them are not necessary in an Isabelle representation.
BibTex
@inproceedings{ckkp-cicm17, author = {Cezary Kaliszyk and Karol Pak}, title = {Presentation and Manipulation of {M}izar Properties inan {I}sabelle Object Logic}, pages = {193--207}, doi = {10.1007/978-3-319-62075-6_14}, booktitle = {10th International Conference on Intelligent ComputerMathematics (CICM'17)}, year = {2017}, editor = {Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke}, series = {LNCS}, volume = {10383}, publisher = {Springer},}
- Details
- Category: Publications 2017
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 83-98, 2017.
pdf doi:10.1007/978-3-319-62075-6_7
Abstract
Mathematical knowledge is publicly available in dozens of different formats and languages, ranging from informal (e.g. Wikipedia) to formal corpora (e.g., Mizar). Despite an enormous amount of overlap between these corpora, only few machine-actionable connections exist. We speak of alignment if the same concept occurs in different libraries, possibly with slightly different names, notations, or formal definitions. Leveraging these alignments creates a huge
potential for knowledge sharing and transfer, e.g., integrating theorem provers or reusing services across systems. Notably, even imperfect alignments, i.e. concepts that are very similar rather than identical, can often play very important roles. Specifically, in machine learning techniques for theorem proving and in automation techniques that use these, they allow learning-reasoning based automation for theorem provers to take inspiration from proofs from different formal proof libraries or semi-formal libraries even if the latter is based on a different mathematical foundation. We present a classification of alignments and design a simple format for describing alignments, as well as an infrastructure for sharing them. We propose these as a centralized standard for the community. Finally, we present an initial collection of ≈12000 alignments from the different kinds of mathematical corpora, including proof assistant libraries and semi-formal corpora as a public resource.
BibTex
@inproceedings{dmtgckmkfrcicm17, author = {Dennis M{\"{u}}ller and Thibault Gauthier and Cezary Kaliszyk and Michael Kohlhase and Florian Rabe}, title = {Classification of Alignments Between Concepts of FormalMathematical Systems}, booktitle = {10th International Conference on Intelligent ComputerMathematics (CICM'17)}, pages = {83--98}, year = {2017}, doi = {10.1007/978-3-319-62075-6_7}, editor = {Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke}, series = {LNCS}, volume = {10383}, publisher = {Springer},}
- Details
- Category: Publications 2017
Michael Färber, Cezary Kaliszyk, Josef Urban
26th International Conference on Automated Deduction, LNCS 10395, pp. 563-579, 2017.
pdf doi:10.1007/978-3-319-63046-5_34
Abstract
We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from previous proofs. We present an implementation based on the leanCoP prover. The system is trained and evaluated on a large suite of related problems coming from the Mizar proof assistant, showing that it is capable to find new and different proofs.
BibTex
@inproceedings{mfckju-cade17, author = {Michael F{\"{a}}rber and Cezary Kaliszyk and Josef Urban}, title = {Monte Carlo Tableau Proof Search}, booktitle = {26th International Conference on Automated Deduction(CADE 2017)}, pages = {563--579}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-63046-5_34}, doi = {10.1007/978-3-319-63046-5_34}, editor = {Leonardo de Moura}, series = {LNCS}, volume = {10395}, publisher = {Springer},}
- Details
- Category: Publications 2017
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017.
pdf doi:10.1007/978-3-319-63046-5_24
Abstract
CSI is a strong automated confluence prover for rewrite systems which has been in development since 2010. In this paper we report on recent extensions that make CSI more powerful, secure, and useful. These extensions include improved confluence criteria but also support for uniqueness of normal forms. Most of the implemented techniques produce machine-readable proof output that can be independently verified by an external tool, thus increasing the trust in CSI. We also report on CSI^ho, a tool built on the same framework and similar ideas as CSI that automatically checks confluence of higher-order rewrite systems.
BibTex
@inproceedings{JNBFAM-CADE17, author = "Julian Nagele and Bertram Felgenhauer and Aart Middeldorp", title = "{CSI}: New Evidence --- A Progress Report", booktitle = "Proceedings of the 26th International Conference on Automated Deduction (CADE-26)", editor = "Leonardo de Moura", series = "Lecture Notes in Artificial Intelligence", volume = 10395, pages = "385--397", year = 2017, doi = "10.1007/978-3-319-63046-5_24"}
- Details
- Category: Publications 2017
Christian Sternagel, Thomas Sternagel
Proceedings of the 26th International Confluence on Automated Deduction, LNCS 10395, pp. 413-431, 2017.
pdf doi:10.1007/978-3-319-63046-5_26
Abstract
We formalize a confluence criterion for the class of quasi-decreasing strongly deterministic conditional term rewrite systems in Isabelle/HOL: confluence follows if all conditional critical pairs are joinable. However, quasi-decreasingness, strong determinism, and joinability of conditional critical pairs are all undecidable in general. Therefore, we also formalize sufficient criteria for those properties, which we incorporate into the general purpose certifier CeTA
as well as the confluence checker ConCon for conditional term rewrite systems.
BibTex
@inproceedings{CSTS-CADE17, author = "Christian Sternagel and Thomas Sternagel", title = "Certifying Confluence of Quasi-Decreasing StronglyDeterministic Conditional Term Rewrite Systems", booktitle = "Proceedings of the 26th International Confluence onAutomated Deduction (CADE-26)", editor = "de Moura L.", series = "Lecture Notes in Computer Science", volume = 10395, pages = "413-431", year = 2017, doi = "10.1007/978-3-319-63046-5_26"}
- Details
- Category: Publications 2017
Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
Proceedings of the 26th International Confluence on Automated Deduction, Lecture Notes in Computer Science 10395, pp. 454-471, 2017.
pdf doi:10.1007/978-3-319-63046-5_28
Springer International Publishing AG
Abstract
Modern program analyzers translate imperative programs to an intermediate formal language like integer transition systems (ITSs), and then analyze properties of ITSs. Because of the high complexity of the task, a number of incorrect proofs are revealed annually in the Software Verification Competitions.
In this paper, we establish the trustworthiness of termination and safety proofs for ITSs. To this end we extend our Isabelle/HOL formalization IsaFoR by formalizing several verification techniques for ITSs, such as invariant checking, ranking functions, etc. Consequently the extracted certifier CeTA can now (in)validate safety and termination proofs for ITSs. We also adapted the program analyzers T2 and AProVE to produce machine-readable proof certificates, and as a result, most termination proofs generated by these tools on a standard benchmark set are now certified.
BibTex
@inproceedings{MBSJRTAY-CADE17, author = {Marc Brockschmidt and Sebastiaan J. C. Joosten and Ren{\'{e}} Thiemann and Akihisa Yamada}, editor = {Leonardo de Moura}, title = {Certifying Safety and Termination Proofs for Integer Transition Systems}, booktitle = {Proceedings of the 26th International Conference on Automated Deduction (CADE 2017)}, series = {Lecture Notes in Computer Science}, volume = {10395}, pages = {454--471}, publisher = {Springer}, year = {2017}, doi = {http://dx.doi.org/10.1007/978-3-319-63046-5_28},}
- Details
- Category: Publications 2017
Cezary Kaliszyk, Josef Urban, Jiřı́ Vyskočil
8th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10499, pp. 12 – 27, 2017.
pdf doi:10.1007/978-3-319-66107-0_2
Standard Springer LNCS Copyright
Abstract
We discuss the progress in our project which aims to automate formalization by combining natural language processing with deep semantic understanding of mathematical expressions. We introduce the overall motivation and ideas behind this project, and then propose a context-based parsing approach that combines efficient statistical learning of deep parse trees with their semantic pruning by type checking and large-theory automated theorem proving. We show that our learning method allows efficient use of large amount of contextual information, which in turn significantly boosts the precision of the statistical parsing and also makes it more efficient. This leads to a large improvement of our first results in parsing theorems from the Flyspeck corpus.
BibTex
@inproceedings{ckjujv-itp17, author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il}, title = {Automating Formalization by Statistical and Semantic Parsing of Mathematics}, booktitle = {8th International Conference on Interactive Theorem Proving (ITP 2017)}, pages = {12--27}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-66107-0_2}, doi = {10.1007/978-3-319-66107-0_2}, editor = {Mauricio Ayala{-}Rinc{\'{o}}n and C{\'{e}}sar A. Mu{\~{n}}oz}, series = {Lecture Notes in Computer Science}, volume = {10499}, publisher = {Springer},}
- Details
- Category: Publications 2017