Julian Nagele
PhD thesis, University of Innsbruck, 2017.
Abstract
This thesis is devoted to the mechanized confluence analysis of rewrite systems. Rewrite systems consist of directed equations and computation is performed by successively replacing instances of left-hand sides of equations by the corresponding instance of the right-hand side. Confluence is a fundamental property of rewrite systems, which ensures that different computation paths produce the same result. Since rewriting is Turing-complete, confluence is undecidable in general. Nevertheless, techniques have been developed that can be used to determine confluence for many rewrite systems and several automatic confluence provers are under active development. Our goal is to improve three aspects of automatic confluence analysis, namely (a) reliability, (b) power, and© versatility. The importance of these aspects is witnessed by the annual international confluence competition, where the leading automated tools analyze confluence of rewrite systems. To improve the reliability of automatic confluence analysis, we formalize confluence criteria for rewriting in the proof assistant Isabelle/HOL, resulting in a verified, executable checker for confluence proofs. To enhance the power of confluence tools, we present a remarkably simple technique, based on the addition and removal of redundant equations, that strengthens existing techniques. To make automatic confluence analysis more versatile, we develop a higher-order confluence tool, making automatic confluence analysis applicable to systems with functional and bound variables.
BibTex
@phdthesis{JN17, author = "Julian Nagele", title = "Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order Rewrite Systems", school = "University of Innsbruck", year = 2017}
- Details
- Category: Publications 2018
Christian Sternagel, René Thiemann
Archive of Formal Proofs, 2018.
Abstract
We formalize basic results on first-order terms, including a first-order unification algorithm, as well as well-foundedness of the subsumption order. This entry is part of the Isabelle Formalization of Rewriting IsaFoR, where first-order terms are omni-present: the unification algorithm is used to certify several confluence and termination techniques, like critical-pair computation and dependency graph approximations; and the subsumption order is a crucial ingredient for completion.
BibTex
@article{CSRT-AFP18, author = {Christian Sternagel and René Thiemann}, title = {First-Order Terms}, journal = {Archive of Formal Proofs}, month = feb, year = 2018, note = {\url{https://www.isa-afp.org/entries/First_Order_Terms.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2018
Julian Parsert, Cezary Kaliszyk
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 91-101, 2018.
Abstract
Economic activity has always been a fundamental part of society. With recent social and political changes economics has gained even more influence on our lives. In this paper we formalize two economic models in Isabelle/HOL: the pure exchange economy, where the only economic actors are consumers, as well as a version of the Arrow-Debreu Model, a private ownership economy, which includes production facilities. Interestingly, the definitions of various components of the economic models differ in the economic literature. We therefore show the equivalences and implications between various presentations, which allows us to create an extensible foundation for formalizing microeconomics and game theory compatible with multiple economic theories. We prove the First Theorem of Welfare Economics in both economic models. The theorem is the mathematical formulation of Adam Smith’s famous invisible hand and states that a group of self-interested and rational actors will eventually achieve an efficient allocation of goods. The formal proofs allow us to find more precise assumptions than those found in the economic literature.
BibTex
@inproceedings{JPKC_CPP_2018, author = {Parsert, Julian and Kaliszyk, Cezary}, title = {Formal Microeconomic Foundations and the First Welfare Theorem}, booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs}, series = {CPP 2018}, year = {2018}, pages = {91--101}, doi = {10.1145/3167100}, publisher = {ACM}}
- Details
- Category: Publications 2018
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 2-13, 2018.
Abstract
Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^n for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations.
In this work we formalize the Perron-Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a non-trivial case study for these Isabelle tools.
BibTex
@inproceedings{JDSJOKRTAY_CPP2018, author = {Divas\'{o}n, Jose and Joosten, Sebastiaan and Kun\v{c}ar, Ond\v{r}ej and Thiemann, Ren{\'e} and Yamada, Akihisa}, title = {Efficient Certification of Complexity Proofs: Formalizing the {P}erron--{F}robenius Theorem (Invited Talk Paper)}, booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs}, series = {CPP 2018}, year = {2018}, pages = {2--13}, doi = {10.1145/3167103}, publisher = {ACM},}
- Details
- Category: Publications 2018
Ralph Bottesch, Jose Divasón, Max Haslbeck, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2018.
Abstract
The Lenstra-Lenstra-Lovász basis reduction algorithm, also known as LLL algorithm, is an algorithm to find a basis with short, nearly orthogonal vectors of an integer lattice. Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), which is an NP-hard problem, where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm also possesses many applications in diverse fields of computer science, from cryptanalysis to number theory, but it is specially well-known since it was used to implement the first polynomial-time algorithm to factor polynomials. In this work we present the first mechanized soundness proof of the LLL algorithm to compute short vectors in lattices. The formalization follows a textbook by von zur Gathen and Gerhard.
BibTex
@article{LLL_Basis_Reduction-AFP, author = {Ralph Bottesch and Jose Divas\'on and Max Haslbeck and Sebastiaan Joosten and Ren\'e Thiemann and Akihisa Yamada}, title = {A verified LLL algorithm}, journal = {Archive of Formal Proofs}, month = feb, year = 2018, note = {\url{http://isa-afp.org/entries/LLL_Basis_Reduction.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2018
Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2018.
Abstract
Short vectors in lattices and factors of integer polynomials are related. Each factor of an integer polynomial belongs to a certain lattice. When factoring polynomials, the condition that we are looking for an irreducible polynomial means that we must look for a small element in a lattice, which can be done by a basis reduction algorithm. In this development we formalize this connection and thereby one main application of the LLL basis reduction algorithm: an algorithm to factor square-free integer polynomials which runs in polynomial time. The work is based on our previous Berlekamp–Zassenhaus development, where the exponential reconstruction phase has been replaced by the polynomial-time basis reduction algorithm. Thanks to this formalization we found a serious flaw in a textbook.
BibTex
@article{LLL_Factorization-AFP, author = {Jose Divas\'on and Sebastiaan Joosten and Ren\'e Thiemann and Akihisa Yamada}, title = {A verified factorization algorithm for integer polynomials with polynomial complexity}, journal = {Archive of Formal Proofs}, month = feb, year = 2018, note = {\url{http://isa-afp.org/entries/LLL_Factorization.html}, Formal proof development}, ISSN = {2150-914x}}
- Details
- Category: Publications 2018
Łukasz Czajka, Cezary Kaliszyk
J. Autom. Reasoning 61, pp. 423 – 453, 2018.
pdf 
doi:10.1007/s10817-018-9458-4
Abstract
Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, the construction of hammers for such foundations has been hindered so far by the lack of translation and reconstruction components. In this paper, we present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is “sufficiently” sound and complete to be of practical use for automated theorem provers. We also introduce a proof reconstruction mechanism based on an eauto-type algorithm combined with limited rewriting, congruence closure and some forward reasoning. The algorithm is able to re-prove in the Coq logic most of the theorems established by the ATPs. Together wih machine-learning based selection of relevant premises this constitutes a full hammer system. The performance of the whole procedure is evaluated in a bootstrapping scenario emulating the development of the Coq standard library. For each theorem in the library only the previous theorems and proofs can be used. We show that 40.8% of the theorems can be proved in a push-button mode in about 40 seconds of real time on a 8-CPU system.
BibTex
@article{lcck-jar18, author = {\L{}ukasz Czajka and Cezary Kaliszyk}, title = {Hammer for {C}oq: Automation for Dependent Type Theory}, journal = {J. Autom. Reasoning}, volume = {61}, number = {1-4}, pages = {423--453}, year = {2018}, url = {https://doi.org/10.1007/s10817-018-9458-4}, doi = {10.1007/s10817-018-9458-4}, }
- Details
- Category: Publications 2018
Arpan Kabira, T. V. H. Prathamesh, Rishi Vyas
International Journal of Algebra and Computation 28, pp. 331-344, 2018.
pdf doi:10.1142/S0218196718500157
Abstract
Irreducible Artin groups of finite type can be parametrized via their associated Coxeter diagrams into six sporadic examples and four infinite families, each of which is further parametrized by the natural numbers. Within each of these four infinite families, we investigate the relationship between elementary equivalence and isomorphism. For three out of the four families, we show that two groups in the same family are equivalent if and only if they are isomorphic; a positive, but weaker, result is also attained for the fourth family. In particular, we show that two braid groups are elementarily equivalent if and only if they are isomorphic. The (∀∃)1 fragment suffices to distinguish the elementary theories of the groups in question.
As a consequence of our work, we prove that there are infinitely many elementary equivalence classes of irreducible Artin groups of finite type. We also show that mapping class groups of closed surfaces – a geometric analogue of braid groups – are elementarily equivalent if and only if they are isomorphic.
BibTex
@article{KPV_IJAC_18, author = {Kabiraj, Arpan and Prathamesh, T. V. H. and Vyas, Rishi}, title = {Elementary equivalence in {A}rtin groups of finite type}, journal = {International Journal of Algebra and Computation}, volume = {28}, number = {02}, pages = {331-344}, year = {2018}, doi = {10.1142/S0218196718500157}}
- Details
- Category: Publications 2018
Thibault Gauthier
PhD thesis, University of Innsbruck, 2018.
pdf doi:10.1016/j.jsc.2018.04.005
Abstract
One of the aims of artificial intelligence is to be able to solve problems through learning and automated reasoning. Famous examples of intelligent systems can be found in molecular chemistry and games such as chess and Go. The current most successful approaches in these domains combine statistical models trained by machine learning methods with search strategies. However, more abstract problems, generally out of reach of current methods, constructed from abstract principles such as induction appear commonly in mathematics. And proving new theorems often requires to exploit patterns hidden in complex structures. The aim of this thesis is to improve automated reasoning techniques in mathematics. This would help to reduce the time needed for formally proving complex theorems such as the Kepler conjecture. In order for our system to learn from a large number of examples, we align the formal libraries of interactive theorem provers (ITPs) by recognizing similar concepts. The shared knowledge is processed by a statistical model which infers relations between mathematical objects. We exploit those links to produce better strategies for proving theorems. In practice, our project combines ITP knowledge with the search power of automated theorem provers (ATPs). Therefore, if a mathematician states a conjecture in an ITP, our system understands through the statistical model the relation of the conjecture to previously formalized knowledge. It selects theorems relevant for proving the conjecture, simplifies the proof by conjecturing intermediate lemmas and may also guide the proof search by choosing suitable reasoning methods. If successful, it produces a computer-verified proof of the conjecture.
BibTex
@phdthesis{TG18, author = "Thibault Gauthier", title = "Learning-Assisted Reasoning within Proof Assistants", school = "University of Innsbruck", year = 2018}
- Details
- Category: Publications 2018
Thibault Gauthier, Cezary Kaliszyk
J. Symbolic Computation 90, pp. 89 – 123, 2018.
pdf doi:10.1016/j.jsc.2018.04.005
Abstract
As the knowledge available in the computer understandable proof corpora grows, recognizing repeating patterns becomes a necessary requirement in order to organize, synthesize, share, and transmit ideas. In this work, we automatically discover patterns in the libraries of interactive theorem provers and thus provide the basis for such applications for proof assistants. This involves detecting close properties, inducing the presence of matching concepts, as well as dynamically evaluating the quality of matches from the similarity of the environment of each concept. We further propose a classification process, which involves a disambiguation mechanism to decide which concepts actually represent the same mathematical ideas. We evaluate the approach on the libraries of six proof assistants based on different logical foundations: HOL4, HOL Light, and Isabelle/HOL for higher-order logic, Coq and Matita for intuitionistic type theory, and the Mizar Mathematical Library for set theory. Comparing the structures available in these libraries our algorithm automatically discovers hundreds of isomorphic concepts and thousands of highly similar ones.
BibTex
@Article{tgck-jsc18, author = {Thibault Gauthier and Cezary Kaliszyk}, title = {Aligning Concepts across Proof Assistant Libraries}, journal = {J. Symbolic Computation}, volume = {90}, pages = {89--123}, year = {2019}, url = {https://doi.org/10.1016/j.jsc.2018.04.005}, doi = {10.1016/j.jsc.2018.04.005},}
- Details
- Category: Publications 2018
Franziska Rapp, Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 81 – 88, 2018.
pdf doi:10.1007/978-3-319-94205-6_6
Springer International Publishing AG
Abstract
FORT is a tool that implements the first-order theory of rewriting for the decidable class of left-linear right-ground rewrite systems. It can be used to decide properties of a given rewrite system and to synthesize rewrite systems that satisfy arbitrary properties expressible in the first-order theory of rewriting. In this paper we report on the extensions that were incorporated in the latest release (2.0) of FORT. These include witness generation for existentially quantified variables in formulas, support for combinations of rewrite systems, as well as an extension to deal with non-ground terms for properties related to confluence.
BibTex
@inproceedings{FRAM-IJCAR18, author = "Franziska Rapp and Aart Middeldorp", title = "{FORT} 2.0", booktitle = "Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2019)", editor = "Didier Galmiche and Stephan Schulz and Roberto Sebastiani", series = "Lecture Notes in Artificial Intelligence", volume = 10900, pages = "81--88", year = 2018, doi = "10.1007/978-3-319-94205-6_6"}
- Details
- Category: Publications 2018
Nao Hirokawa, Julian Nagele, and Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018), Lecture Notes in Artificial Intelligence 10900, pp. 346 – 353, 2018.
pdf doi:10.1007/978-3-319-94205-6_23
Springer International Publishing AG
Abstract
In this paper we describe the infrastructure supporting confluence tools and competitions: Cops, the confluence problems database, and CoCoWeb, a convenient web interface for tools that participate in the annual confluence competition.
BibTex
@inproceedings{NHJNAM-IJCAR18, author = "Nao Hirokawa and Julian Nagele and Aart Middeldorp", title = "Cops and {CoCoWeb}: Infrastructure for Confluence Tools", booktitle = "Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2019)", editor = "Didier Galmiche and Stephan Schulz and Roberto Sebastiani", series = "Lecture Notes in Artificial Intelligence", volume = 10900, pages = "346--353", year = 2018, doi = "10.1007/978-3-319-94205-6_23"}
- Details
- Category: Publications 2018
Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 441 – 458, 2018.
pdf doi:10.1007/978-3-319-94821-8_26
Abstract
In this work we are interested in minimal complete sets of solutions for homogeneous linear diophantine equations. Such equations naturally arise during AC-unification, that is, unification in the presence of associative and commutative symbols. Minimal complete sets of solutions are for example required to compute AC-critical pairs. We present a verified solver for homogeneous linear diophantine equations that we formalized in Isabelle/HOL. Our work provides the basis for formalizing AC-unification and will eventually enable the certification of automated AC-confluence and AC-completion tools.
BibTex
@inproceedings{FMJPJSCS-ITP18, author = "Florian Me\ss{}ner, Julian Parsert, Jonas Sch\"opf, Christian Sternagel", title = "A Formally Verified Solver for Homogeneous Linear Diophantine Equations", booktitle = "Proceedings of the 9th International Conference on Interactive Theorem Proving", editor = "Jeremy Avigad and Assia Mahboubi", series = "Lecture Notes in Computer Science", volume = 10895, pages = "441--458", year = 2018, doi = "10.1007/978-3-319-94821-8_26"}
- Details
- Category: Publications 2018
Bertram Felgenhauer, Aart Middeldorp, Fabian Mitterwallner, and Julian Nagele
Proceedings of the 7th International Workshop on Confluence (IWC 2018), pp. 76, 2018.
Abstract
The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography.
In this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.
BibTex
@inproceedings{BFAMFMJN-IWC18, author = "Bertram Felgenhauer and Aart Middeldorp and Fabian Mitterwallner and Julian Nagele", title = "{CoCo} 2018 Participant: {CSI} 1.2.1", booktitle = "Proceedings of the 7th International Workshop on Confluence", editor = "Bertram Felgenhauer and Jakob Grue Simonsen", pages = 76, year = 2018}
- Details
- Category: Publications 2018
Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Proceedings of the 9th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 160 – 177, 2018.
pdf http://dx.doi.org/10.1007/978-3-319-94821-8_10
Abstract
The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography.
In this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.
BibTex
@inproceedings{JDSJRTAY-ITP18, title = {A Formalization of the {LLL} Basis Reduction Algorithm}, author = {Jose Divas\'on and Sebastiaan Joosten and Ren\'e Thiemann and Akihisa Yamada}, year = 2018, booktitle = {Proceedings of the 9th International Conference on Interactive Theorem Proving}, editor = {Jeremy Avigad and Assia Mahboubi}, series = {Lecture Notes in Computer Science}, pages = {160--177}, volume = {10895}, doi = {10.1007/978-3-319-94821-8_10}}
- Details
- Category: Publications 2018
Julian Parsert, Cezary Kaliszyk
Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 495 – 503, 2018.
pdf doi:10.1007/978-3-319-94821-8_29
Standard Springer LNCS Copyright
Abstract
Utility functions form an essential part of game theory and economics. In order to guarantee the existence of these utility functions sufficient properties are assumed in an axiomatic manner. In this paper we discuss these axioms and the von-Neumann-Morgenstern Utility Theorem, which names precise assumptions under which expected utility functions exist. We formalize these results in Isabelle/HOL. The formalization includes formal definitions of the underlying concepts including continuity and independence of preferences. We make the dependencies more precise and highlight some consequences for a formalization of game theory.
BibTex
@InProceedings{JPCK-ITP18, author = "Julian Parsert and Cezary Kaliszyk", title = "Towards Formal Foundations for Game Theory", editor = "Jeremy Avigad and Assia Mahboubi", booktitle = "Proceedings of the 9th International Conference on Interactive Theorem Proving", series = "Lecture Notes in Computer Science", volume = 10895, pages = "495--503", year = 2018, doi = "10.1007/978-3-319-94821-8_29"}
- Details
- Category: Publications 2018
Jan Jakubův, Cezary Kaliszyk
6th International Conference on Mathematical Software, Lecture Notes in Computer Science 10931, pp. 245 – 254, 2018.
doi:10.1007/978-3-319-96418-8_29
Standard Springer LNCS Copyright
Abstract
We propose an extension of the automated theorem prover E by the weighted path ordering. Weighted path ordering is theoretically stronger than all the orderings used in E-prover, however its parametrization is more involved than those normally used in automated reasoning. In particular, it depends on a term algebra. We discuss how the parameters for the ordering can be proposed automatically for particular theorem proving problem strategies. We integrate the ordering in E-prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the ones used in E prover so far.
BibTex
@inproceedings{jjck-icms18, author = {Jan Jakubuv and Cezary Kaliszyk}, title = {Towards a Unified Ordering for Superposition-Based Automated Reasoning}, booktitle = {6th International Conference on Mathematical Software (ICMS 2018)}, pages = {245--254}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-96418-8\_29}, doi = {10.1007/978-3-319-96418-8\_29}, editor = {James H. Davenport and Manuel Kauers and George Labahn and Josef Urban}, series = {LNCS}, volume = {10931}, publisher = {Springer}, year = {2018},}
- Details
- Category: Publications 2018
Sarah Winkler and Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 30:1 – 30:18, 2018.
pdf doi:10.4230/LIPIcs.FSCD.2018.30
Abstract
We propose an abstract completion procedure for logically constrained term rewrite systems (LCTRSs). This procedure can be instantiated to both standard Knuth-Bendix completion and ordered completion for LCTRSs, and we present a succinct and uniform correctness proof. A prototype implementation illustrates the viability of the new completion approach.
BibTex
@inproceedings{SWAM-FSCD18, author = "Sarah Winkler and Aart Middeldorp", title = "Completion for Logically Constrained Rewriting", booktitle = "Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)", editor = "H{\'e}l{\`e}ne Kirchner", series = "Leibniz International Proceedings in Informatics" volume = 108, pages = "30:1--30:18", year = 2018, doi = "10.4230/LIPIcs.FSCD.2018.30"}
- Details
- Category: Publications 2018
Christina Kohl and Aart Middeldorp
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics 108, pp. 31:1 – 31:8, 2018.
pdf doi:10.4230/LIPIcs.FSCD.2018.31
Abstract
Proof terms are a useful concept for reasoning about computations in term rewriting. Human calculation with proof terms is tedious and error-prone. We present ProTeM, a new tool that offers support for manipulating proof terms that represent multisteps in left-linear rewrite systems.
BibTex
@inproceedings{CKAM-FSCD18, author = "Christina Kohl and Aart Middeldorp", title = "{ProTeM}: A Proof Term Manipulator (System Description)", booktitle = "Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)", editor = "H{\'e}l{\`e}ne Kirchner", series = "Leibniz International Proceedings in Informatics" volume = 108, pages = "31:1--31:8", year = 2018, doi = "10.4230/LIPIcs.FSCD.2018.31"}
- Details
- Category: Publications 2018
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics 108, pp. 32:1 – 32:5, 2018.
pdf doi:10.4230/LIPIcs.FSCD.2018.32
Abstract
We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.
BibTex
@inproceedings{AHHMNNSZ-FSCD18, author = "Takahito Aoto and Makoto Hamana and Nao Hirokawa and Aart Middeldorp and Julian Nagele and Naoki Nishida and Kiraku Shintani and Harald Zankl", title = "Confluence Competition 2018", booktitle = "Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction", editor = "H{\'e}l{\`e}ne Kirchner", series = "Leibniz International Proceedings in Informatics" volume = 108, pages = "32:1--32:5", year = 2018, doi = "10.4230/LIPIcs.FSCD.2018.32"}
- Details
- Category: Publications 2018
Sarah Winkler, Georg Moser
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 472 – 480, 2018.
pdf doi:10.1007/978-3-319-94205-6_31
Springer International Publishing AG
Abstract
The equational reasoning tool MaedMax implements maximal ordered completion. This new approach extends the maxSMT-based method for standard completion developed by Klein and Hirokawa (2011) to ordered completion and equational theorem proving. MædMax incorporates powerful ground completeness checks and supports certification of its proofs by an Isabelle-based certifier. It also provides an order generation mode which can be used to synthesize term orderings for other tools. Experiments show the potential of our approach.
BibTex
@inproceedings{SWGM-IJCAR18, author = "Sarah Winkler and Georg Moser", title = "MaedMax: A Maximal Ordered Completion Tool", booktitle = "Proceedings of the 9th International Joint Conference on Automated Reasoning", editor = "Didier Galmiche, Stephan Schulz, and Roberto Sebastiani", series = "Lecture Notes in Artificial Intelligence", volume = 10900, pages = "472--480", year = 2018, doi = "10.1007/978-3-319-94205-6_31"}
- Details
- Category: Publications 2018