René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2015.
doi:10.1007/978-3-319-22102-1_28
Abstract
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 partially prove the result that every complex matrix has a Jordan normal form: we are restricted to upper-triangular matrices since we did not yet formalize the 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.
BibTex
@article{Jordan_Normal_Form-AFP, author = "Ren{\'e} Thiemann and Akihisa Yamada", title = "Matrices, Jordan Normal Forms, and Spectral Radius Theory", journal = "Archive of Formal Proofs", year = 2015, note = "{\url{https://www.isa-afp.org/entries/Jordan_Normal_Form.html}}, Formal proof development"}
- Details
- Category: Publications 2015
Christian Sternagel and René Thiemann
Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science 9236, pp. 421 – 437, 2015.
pdf doi:10.1007/978-3-319-22102-1_28
Abstract
We present an Isabelle/HOL development that allows for the automatic generation of certain operations for user-defined datatypes. Since the operations are defined within the logic, they are applicable for code generation. Triggered by the demand to provide readable error messages as well as to access efficient data structures like sorted trees in generated code, we provide show functions that compute the string representation of a given value, comparators that yield linear orders, and hash functions. Moreover, large parts of the employed machinery should be reusable for other operations like read functions, etc.
In contrast to similar mechanisms, like Haskell’s “deriving,” we do not only generate definitions, but also prove some desired properties, e.g., that a comparator indeed orders values linearly. This is achieved by a collection of tactics that discharge the corresponding proof obligations automatically.
BibTex
@inproceedings{CSRT-ITP15, author = "Christian Sternagel and Ren{\'e} Thiemann", title = "Deriving Comparators and Show Functions in {Isabelle/HOL}", booktitle = "Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015)", editor = "Christian Urban and Xingyuan Zhang", series = "Lecture Notes in Computer Science", volume = 9236, pages = "421--437", year = 2015, doi = "10.1007/978-3-319-22102-1_28"}
- Details
- Category: Publications 2015
Martin Avanzini, Ugo Dal Lago, and Georg Moser
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 152 – 164, 2015.
pdf doi:10.1145/2784731.2784753
Abstract
We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalised versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Further, we describe suitable strategies for the application of the studied transformations and provide ample experimental data for assessing the viability of our method.
BibTex
@InProceedings{MAUDLGM15, author = "Martin Avanzini and Ugo Dal Lago and Georg Moser", title = "Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order", booktitle = "Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015)", year = 2015, pages = "152--164", publisher = "ACM", doi = "10.1145/2784731.2784753"}
- Details
- Category: Publications 2015
Cezary Kaliszyk
Proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015), Lecture Notes in Artificial Intelligence 9323, pp. 102 – 111, 2015.
pdf doi:10.1007/978-3-319-24312-2_8
© Springer International Publishing Switzerland
Abstract
Many tableaux provers that follow Stickel’s Prolog Technology and lean have been relying on the Prolog compiler for an efficient term representation and the implementation of unification. In particular, this is the case for leanCOP, the only tableaux prover that regularly takes part in the CASC, the yearly ATP competition. On the other hand, the most efficient superposition provers are typically written in low-level languages, reckoning that the efficiency factor is significant.
In this paper we discuss low-level representations for first-order tableaux theorem proving and present the Bare Metal Tableaux Prover, a C implementation of the exact calculus used in the leanCoP theorem prover with its cut semantics. The data structures are designed in such a way that the prove function does not need to allocate any memory. The code is less elegant than the Prolog code, albeit concise and readable. We also measure the constant factor that a high-level programming language incurs: the low-level implementation performs 18 times more inferences per second on an average TPTP CNF problem. We also discuss the implementation improvements which could be enabled by complete access to the internal data structures, such as direct manipulation of backtracking points.
BibTex
@inproceedings{CK-TABLEAUX15, author = "Cezary Kaliszyk", title = "Efficient Low-Level Connection Tableaux", booktitle = "Proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015)", editor = "Hans de Nivelle", series = "Lecture Notes in Artificial Intelligence", volume = 9323, pages = "102--111", year = 2015, doi = "10.1007/978-3-319-24312-2_8"}
- Details
- Category: Publications 2015
Michael Färber and Cezary Kaliszyk
Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 325 – 340, 2015.
pdf doi:10.1007/978-3-319-24246-0_20
© Springer International Publishing Switzerland
Abstract
The success rates of automated theorem provers in large theories highly depend on the choice of given facts. Premise selection is the task of choosing a subset of given facts, which is most likely to lead to a successful automated deduction proof of a given conjecture. Premise selection can be viewed as a multi-label classification problem, where machine learning from related proofs turns out to currently be the most successful method. Random forests are a machine learning technique known to perform especially well on large datasets. In this paper, we evaluate random forest algorithms for premise selection. To deal with the specifics of automated reasoning, we propose a number of extensions to random forests, such as incremental learning, multi-path querying, depth weighting, feature IDF (inverse document frequency), and integration of secondary classifiers in the tree leaves. With these extensions, we improve on the k-nearest neighbour algorithm both in terms of prediction quality and ATP performance.
BibTex
@inproceedings{MFCK-FROCOS2015, author = "Michael F{\"a}rber and Cezary Kaliszyk", title = "Random Forests for Premise Selection", booktitle = "Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015)", editor = "Carsten Lutz and Silvio Ranise", series = "Lecture Notes in Artificial Intelligence", volume = 9322, pages = "325--340", year = 2015, doi = "10.1007/978-3-319-24246-0_20"}
- Details
- Category: Publications 2015
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil
Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 341 – 356, 2015.
pdf doi:10.1007/978-3-319-24246-0_21
© Springer International Publishing Switzerland
Abstract
In this work we improve ATP performance in large theories by the reuse of lemmas derived in previous related problems. Given a large set of related problems to solve, we run automated theorem provers on them, extract a large number of lemmas from the proofs found and post-process the lemmas to make them usable in the remaining problems. Then we filter the lemmas by several tools and extract their proof dependencies, and use machine learning on such proof dependencies to add the most promising generated lemmas to the remaining problems. On such enriched problems we run the automated provers again, solving more problems. We describe this method and the techniques we used, and measure the improvement obtained. On the MPTP2078 large-theory benchmark the method yields 6.6% and 6.2% more problems proved in two different evaluation modes.
BibTex
@inproceedings{CKJUJV-FROCOS2015, author = "Cezary Kaliszyk and Josef Urban and Ji\v{r}\'i Vysko\v{c}il", title = "Lemmatization for Stronger Reasoning in Large Theories", booktitle = "Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015)", editor = "Carsten Lutz and Silvio Ranise", series = "Lecture Notes in Artificial Intelligence", volume = 9322, pages = "341--356", year = 2015, doi = "10.1007/978-3-319-24246-0_21"}
- Details
- Category: Publications 2015
Sarah Winkler and René Thiemann
Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015), Lecture Notes in Artificial Intelligence 9322, pp. 239 – 255, 2015.
pdf doi:10.1007/978-3-319-24246-0_15
© Springer International Publishing Switzerland
Abstract
Unravelings constitute a class of program transformations to model conditional rewrite systems as standard term rewrite systems. Key properties of unravelings are soundness and completeness with respect to reductions, in the sense that rewrite sequences in the unraveled system correspond to rewrite sequences in the conditional system and vice versa. While the latter is easily satisfied, the former holds only under certain conditions and is notoriously difficult to prove. This paper describes an Isabelle formalization of both properties. The soundness proof is based on the approach by Nishida, Sakai, and Sakabe (2012) but we also contribute to the theory by showing it applicable to a larger class of unravelings.
Based on our formalization we developed the first certifier to check output of conditional rewrite tools. In particular, quasi-decreasingness proofs by AProVE and conditional confluence proofs by ConCon can be certified.
BibTex
@inproceedings{SWRT-FROCOS2015, author = "Sarah Winkler and Ren{\'e} Thiemann", title = "Formalizing Soundness and Completeness of Unravelings", booktitle = "Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015)", editor = "Carsten Lutz and Silvio Ranise", series = "Lecture Notes in Artificial Intelligence", volume = 9322, pages = "239--255", year = 2015, doi = "10.1007/978-3-319-24246-0_15"}
- Details
- Category: Publications 2015
Cezary Kaliszyk and Josef Urban
Journal of Automated Reasoning 55(3), pp. 245 – 256, 2015.
pdf doi:10.1007/s10817-015-9330-8
Open Access
Abstract
As a present to Mizar on its 40th anniversary, we develop an AI/ATP system that in 30 seconds of real time on a 14-CPU machine automatically proves 40 % of the theorems in the latest official version of the Mizar Mathematical Library (MML). This is a considerable improvement over previous performance of large-theory AI/ATP methods measured on the whole MML. To achieve that, a large suite of AI/ATP methods is employed and further developed. We implement the most useful methods efficiently, to scale them to the 150000 formulas in MML. This reduces the training times over the corpus to 1–3 seconds, allowing a simple practical deployment of the methods in the online automated reasoning service for the Mizar users (MizAR).
BibTex
@article{CKJU-JAR15, author = "Cezary Kaliszyk and Josef Urban", title = "{MizAR} 40 for {Mizar} 40" journal = "Journal of Automated Reasoning", volume = 55, number = 3, pages = "245--256", year = 2015, doi = "10.1007/s10817-015-9330-8"}
- Details
- Category: Publications 2015
Michael Färber, Cezary Kaliszyk
Proceedings of the 1st Global Conference on Artificial Intelligence (GCAI 2015), EPiC Series in Computing 36, pp. 127-136, 2015.
Abstract
Metis is an automated theorem prover based on ordered paramodulation. It is widely employed in the interactive theorem provers Isabelle/HOL and HOL4 to automate proofs as well as reconstruct proofs found by automated provers. For both these purposes, the tableaux-based MESON tactic is frequently used in HOL Light. However, paramodulation-based provers such as Metis perform better on many problems involving equality. We created a Metis-based tactic in HOL Light which translates HOL problems to Metis, runs an OCaml version of Metis, and reconstructs proofs in Metis’ paramodulation calculus as HOL proofs. We evaluate the performance of Metis as proof reconstruction method in HOL Light.
BibTex
@inproceedings{GCAI2015:Metis-based_Paramodulation_Tactic_for_HOL_Light, author = "Michael Farber and Cezary Kaliszyk", title = "Metis-based Paramodulation Tactic for {HOL} Light", booktitle = "Proceedings of the 1st Global Conference on Artificial Intelligence (GCAI 2015)", series = "EPiC Series in Computing", volume = 36, pages = "127-136", year = 2015}
- Details
- Category: Publications 2015
Cynthia Kop and Naoki Nishida
Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 549 – 557, 2015.
pdf doi:10.1007/978-3-662-48899-7_38
© Springer-Verlag Berlin Heidelberg 2015
Abstract
This paper discusses Ctrl, a tool to analyse – both automatically and manually – term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and can automatically verify termination, confluence and (to a limited extent) term equivalence using inductive theorem proving. Ctrl also offers a manual mode for inductive theorem proving, allowing support for and verification of “hand-written” term equivalence proofs.
BibTex
@inproceedings{CKNN-LPAR15, author = "Cynthia Kop and Naoki Nishida", title = "Constrained Term Rewriting tooL", booktitle = "Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning", series = "Lecture Notes in Computer Science (Advanced Research in Computing and Software Science)", editor = "Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov", volume = 9450, pages = "549--557", year = 2015, doi = "10.1007/978-3-662-48899-7_38"}
- Details
- Category: Publications 2015
Cezary Kaliszyk and Josef Urban
Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 88 – 96, 2015.
pdf doi:10.1007/978-3-662-48899-7_7
© Springer-Verlag Berlin Heidelberg 2015
Abstract
FEMaLeCoP is a connection tableau theorem prover based on leanCoP which uses efficient implementation of internal learning-based guidance for extension steps. Despite the fact that exhaustive use of such internal guidance can incur a significant slowdown of the raw inferencing process, FEMaLeCoP trained on related proofs can prove many problems that cannot be solved by leanCoP. In particular on the MPTP2078 benchmark, FEMaLeCoP adds 90 (15.7 %) more problems to the 574 problems that are provable by leanCoP. FEMaLeCoP is thus the first AI/ATP system convincingly demonstrating that guiding the internal inference algorithms of theorem provers by knowledge learned from previous proofs can significantly improve the performance of the provers. This paper describes the system, discusses the technology developed, and evaluates the system.
BibTex
@inproceedings{CKJU-LPAR15, author = "Cezary Kaliszyk and Josef Urban", title = "{FEMaLeCoP}: Fairly Efficient Machine Learning Connection Prover", booktitle = "Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)", editor = "Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov", series = "Lecture Notes in Computer Science", volume = 9450, pages = "88--96", year = 2015, doi = "10.1007/978-3-662-48899-7_7"}
- Details
- Category: Publications 2015
Thibault Gauthier and Cezary Kaliszyk
Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450, pp. 372 – 386, 2015.
pdf doi:10.1007/978-3-662-48899-7_26
© Springer-Verlag Berlin Heidelberg 2015
Abstract
New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper we propose and evaluate a number of methods, which strengthen proof automation by learning from proof libraries of different provers. Certain conjectures can be proved directly from the dependencies induced by similar proofs in the other library. Even if exact correspondences are not found, learning-reasoning systems can make use of the association between proved theorems and their characteristics to predict the relevant premises. Such external help can be further combined with internal advice. We evaluate the proposed knowledge-sharing methods by reproving the HOL Light and HOL4 standard libraries. The learning-reasoning system HOLHammer, whose single best strategy could automatically find proofs for 30 % of the HOL Light problems, can prove 40 % with the knowledge from HOL4.
BibTex
@inproceedings{TGCK-LPAR15, author = "Thibault Gauthier and Cezary Kaliszyk", title = "Sharing {HOL4} and {HOL L}ight Proof Knowledge", booktitle = "Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20)", editor = "Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov", series = "Lecture Notes in Computer Science", volume = 9450, pages = "372--386", publisher = "Springer", year = 2015, doi = "10.1007/978-3-662-48899-7_26"}
- Details
- Category: Publications 2015
René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2015.
Abstract
Based on existing libraries for matrices, factorization of rational polynomials, and Sturm’s theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as an implementation for real and complex numbers, and it admits to compute roots and completely factorize real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, or a faster but approximative version.
To this end, we mechanized several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain.
BibTex
@article{Algebraic_Numbers-AFP,author = “Ren{\‘e} Thiemann and Akihisa Yamada”,title = “Algebraic Numbers in {I}sabelle/{HOL}”,journal = “Archive of Formal Proofs”,year = 2015,note = {\url{http://isa-afp.org/entries/Algebraic_Numbers.shtml}, Formal proof development}}
- Details
- Category: Publications 2015