René Thiemann
Archive of Formal Proofs 2022.
Abstract
We formalize the weak and strong duality theorems of linear programming. For the strong duality theorem we provide three sufficient preconditions: both the primal problem and the dual problem are satisfiable, the primal problem is satisfiable and bounded, or the dual problem is satisfiable and bounded. The proofs are based on an existing formalization of Farkas’ Lemma.
BibTex
@article{LP_Duality-AFP, author = {René Thiemann}, title = {Duality of Linear Programming}, journal = {Archive of Formal Proofs}, month = {February}, year = {2022}, note = {\url{https://isa-afp.org/entries/LP_Duality.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022
Alexander Lochmann, Bertram Felgenhauer
Archive of Formal Proofs 2022 2022.
Abstract
The first-order theory of rewriting (FORT) is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata technique and an inference system presented in “Certifying Proofs in the First-Order Theory of Rewriting”. This AFP entry provides a formalization of the underlying decision procedure. Moreover it allows to generate a function that can verify each inference step via the code generation facility of Isabelle/HOL. Additionally it contains the specification of a certificate language (that allows to state proofs in FORT) and a formalized function that allows to verify the validity of the proof. This gives software tool authors, that implement the decision procedure, the possibility to verify their output.
BibTex
@article{FO_Theory_Rewriting-AFP, author = {Alexander Lochmann and Bertram Felgenhauer}, title = {First-Order Theory of Rewriting}, journal = {Archive of Formal Proofs}, month = feb, year = 2022, note = {\url{https://isa-afp.org/entries/FO_Theory_Rewriting.html}, Formal proof development}, ISSN = {2150-914x}, }
- Details
- Category: Publications 2022
Manuel Eberl
2022
Abstract
In this article, I formalise a proof from THE BOOK; namely a formula that was called ‘one of the most beautiful formulas involving elementary functions’: π cot(πz) = 1/z + ∑ (1/(z+n) + 1/(z-n)) where the sum ranges over all integers n > 0. The proof uses Herglotz’s trick to show the real case and analytic continuation for the complex case.
BibTex
@article{Cotangent_PFD_Formula-AFP, author = {Manuel Eberl}, title = {A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent}, journal = {Archive of Formal Proofs}, month = {March}, year = {2022}, note = {\url{https://isa-afp.org/entries/Cotangent_PFD_Formula.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022
Stanisław Purgał and Cezary Kaliszyk
Proceedings of the Thirty-Fifth International Florida Artificial Intelligence Research Society Conference, 2022.
pdf 
doi:10.32473/flairs.v35i.130648
Abstract
Existing approaches to learning to prove theorems focuson particular logics and datasets. In this work, we proposeMonte-Carlo simulations guided by reinforcement learningthat can work in an arbitrarily specified logic, without any hu-man knowledge or set of problems. Since the algorithm doesnot need any training dataset, it is able to learn to work withany logical foundation, even when there is no body of proofsor even conjectures available. We practically demonstrate thefeasibility of the approach in multiple logical systems. Theapproach is stronger than training on randomly generated databut weaker than the approaches trained on tailored axiom andconjecture sets. It however allows us to apply machine learn-ing to automated theorem proving for many logics, where nosuch attempts have been tried to date, such as intuitionisticlogic or linear logic.
BibTex
@inproceedings{spck-flairs22, author = {Stanisław Purgał and Cezary Kaliszyk}, booktitle = {Proceedings of the Thirty-Fifth International Florida Artificial Intelligence Research Society Conference, {FLAIRS} 2022}, doi = {10.32473/flairs.v35i.130648}, editor = {Roman Bart{\'{a}}k and Fazel Keshtkar and Michael Franklin}, title = {Adversarial Learning to Reason in an Arbitrary Logic}, url = {https://doi.org/10.32473/flairs.v35i.130648}, year = {2022}}
- Details
- Category: Publications 2022
Manuel Eberl
Archive of Formal Proofs 2022.
Abstract
This article provides a brief formalisation of the two equations known as the Sophomore’s Dream, first discovered by Johann Bernoulli in 1697.
BibTex
@article{Sophomores_Dream-AFP, author = {Manuel Eberl}, title = {The Sophomore's Dream}, journal = {Archive of Formal Proofs}, month = {April}, year = {2022}, note = {\url{https://isa-afp.org/entries/Sophomores_Dream.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022
René Thiemann, Lukas Schmidinger
Archive of Formal Proofs 2022.
Abstract
We consider the problem of comparing two multisets via the generalized multiset ordering. We show that the corresponding decision problem is NP-complete. To be more precise, we encode multiset-comparisons into propositional formulas or into conjunctive normal forms of quadratic size; we further prove that satisfiability of conjunctive normal forms can be encoded as multiset-comparison problems of linear size. As a corollary, we also show that the problem of deciding whether two terms are related by a recursive path order is NP-hard, provided the recursive path order is based on the generalized multiset ordering.
BibTex
@article{Multiset_Ordering_NPC-AFP, author = {René Thiemann and Lukas Schmidinger}, title = {The Generalized Multiset Ordering is NP-Complete}, journal = {Archive of Formal Proofs}, month = {April}, year = {2022}, note = {\url{https://isa-afp.org/entries/Multiset_Ordering_NPC.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022
René Thiemann
Archive of Formal Proofs 2022.
Abstract
Given a graph G with n vertices and a number s, the decision problem Clique asks whether G contains a fully connected subgraph with s vertices. For this NP-complete problem there exists a non-trivial lower bound: no monotone circuit of a size that is polynomial in n can solve Clique. This entry provides an Isabelle/HOL formalization of a concrete lower bound (the bound is (n1/7)n1/8 for the fixed choice of s = n1/4), following a proof by Gordeev.
BibTex
@article{Clique_and_Monotone_Circuits-AFP, author = {René Thiemann}, title = {Clique is not solvable by monotone circuits of polynomial size}, journal = {Archive of Formal Proofs}, month = {May}, year = {2022}, note = {\url{https://isa-afp.org/entries/Clique_and_Monotone_Circuits.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022
Jose Divasón, René Thiemann
Journal of Automated Reasoning online first, 2022.
pdf doi:10.1007/s10817-022-09631-5
Abstract
This work presents formal correctness proofs in Isabelle/HOL of algorithms to transform a matrix into Smith normal form, a canonical matrix form, in a general setting: the algorithms are written in an abstract form and parameterized by very few simple operations. We formally show their soundness provided the operations exist and satisfy some conditions, which always hold on Euclidean domains. We also provide a formal proof on some results about the generality of such algorithms as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out by switching conveniently between two different existing libraries by means of the lifting and transfer package and the use of local type definitions, a sound extension to HOL.
BibTex
@article{JDRT22, author = {Jose Divas{\'{o}}n and Ren{\'{e}} Thiemann}, title = {A Formalization of the Smith Normal Form in Higher-Order Logic}, journal = {J. Autom. Reason.}, volume = {online first}, year = {2022}, doi = {10.1007/s10817-022-09631-5},}
- Details
- Category: Publications 2022
Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 228, pp. 27:1-27:17, 2022.
pdf doi:10.4230/LIPIcs.FSCD.2022.27
Abstract
In this paper we prove via a reduction from Hilbert’s 10th problem that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable, even for rewrite systems that are incrementally polynomially terminating. We also prove that incremental polynomial termination is an undecidable property of terminating rewrite systems.
BibTex
@inproceedings{FMAM-FSCD22, author = "Fabian Mitterwallner and Aart Middeldorp", title = "Polynomial Termination over $\mathbb{N}$ is Undecidable", booktitle = "Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction", editor = "Amy Felty", series = "Leibniz International Proceedings in Informatics" volume = 228, pages = "27:1--27:17", year = 2022, doi = "10.4230/LIPIcs.FSCD.2022.27"}
- Details
- Category: Publications 2022
Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022), pp. 42-47, 2022.
Abstract
Conversion equivalence and normalization equivalence are important properties of two rewrite systems. We investigate how many constants are needed to reduce these properties to their ground versions for linear variable-separated rewrite systems. Our results are implemented in the decision tool FORT-h and formalized in Isabelle/HOL. The latter enables the validation of the proofs produced by the former in the certifier FORTify.
BibTex
@inproceedings{ALFMAM-IWC22, author = "Alexander Lochmann and Fabian Mitterwallner and Aart Middeldorp", title = "Formalized Signature Extension Results for Equivalence", booktitle = "Proceedings of the 11th International Workshop on Confluence", pages = "42--47", year = 2022}
- Details
- Category: Publications 2022
Manuel Eberl
Archive of Formal Proofs 2022.
Abstract
This article provides a formalisation of the Weighted Arithmetic–Geometric Mean Inequality. As a corollary, the regular arithmetic–geometric mean inequality follows. I follow Pólya’s elegant proof, which uses the inequality exp(x) ≥ 1 + x as a starting point. Pólya claims that this proof came to him in a dream, and that it was “the best mathematics he had ever dreamt.”
BibTex
@article{Weighted_Arithmetic_Geometric_Mean-AFP, author = {Manuel Eberl}, title = {Pólya’s Proof of the Weighted Arithmetic–Geometric Mean Inequality}, journal = {Archive of Formal Proofs}, month = {July}, year = {2022}, note = {\url{https://isa-afp.org/entries/Weighted_Arithmetic_Geometric_Mean.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022
Christina Kohl, Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022), pp. 2-6, 2022.
Abstract
Having development closed critical pairs is a well-known sufficient condition for confluence of left-linear term rewrite systems. We present formalized results involving proof terms and unification that play an important role in the proof.
BibTex
@inproceedings{CKAM-IWC22, author = "Christina Kohl and Aart Middeldorp", title = "Development Closed Critical Pairs: Towards a Formalized Proof", booktitle = "Proceedings of the 11th International Workshop on Confluence", pages = "2--6", year = 2022}
- Details
- Category: Publications 2022
Chad E. Brown, Cezary Kaliszyk
Automated Reasoning – 11th International Joint Conference, IJCAR 2022, pp. 250-358, 2022.
pdf doi:10.1007/978-3-031-10769-6_21
Abstract
Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules only use shallow information about the terms and formulas taking part in the rule. Lash uses new, efficient C representations of vital structures and operations. Most importantly, Lash uses a C representation of (normal) terms with perfect sharing along with a C implementation of normalizing substitutions. We describe the ways in which Lash differs from Satallax and the performance improvement of Lash over Satallax when used with analogous flag settings. With a 10 s timeout Lash outperforms Satallax on a collection TH0 problems from the TPTP. We conclude with ideas for continuing the development of Lash.
BibTex
@inproceedings{cbck-ijcar22, author = {Chad E. Brown and Cezary Kaliszyk}, booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022}, doi = {10.1007/978-3-031-10769-6\_21}, editor = {Jasmin Blanchette and Laura Kov{\'{a}}cs and Dirk Pattinson}, pages = {350--358}, publisher = {Springer}, series = {LNCS}, title = {Lash 1.0 (System Description)}, url = {https://doi.org/10.1007/978-3-031-10769-6\_21}, volume = {13385}, year = {2022}}
- Details
- Category: Publications 2022
Stanisław Purgał, David Cerna, Cezary Kaliszyk
31st International Joint Conference on Artificial Intelligence, IJCAI 2022, pp. 2726-2733, 2022.
doi:10.24963/ijcai.2022/378 Open access
Abstract
Learning complex programs through inductive logic programming (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile Learning From Failures paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Our theoretical framework captures a class of higher-order definitions preserving soundness of existing subsumption-based pruning methods.
BibTex
@inproceedings{spdcck-ijcai22, author = {Stanisław Purgał and David Cerna and Cezary Kaliszyk}, booktitle = {Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, {IJCAI} 2022}, doi = {10.24963/ijcai.2022/378}, editor = {Luc De Raedt}, pages = {2726--2733}, publisher = {ijcai.org}, title = {Learning Higher-Order Programs without Meta-Interpretive Learning}, url = {https://doi.org/10.24963/ijcai.2022/378}, year = {2022}}
- Details
- Category: Publications 2022
Karol Pąk, Cezary Kaliszyk
13th International Conference on Interactive Theorem Proving, ITP 2022, pp. 26:1—26:8, 2022.
pdf doi:10.4230/LIPIcs.ITP.2022.26
Abstract
The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step in the negative resolution of Hilbert’s 10th problem. Almost three decades of work on the problem have resulted in several equally surprising results. These include the existence of diophantine equations with a reduced number of variables, as well as the explicit construction of polynomials that represent specific sets, in particular the set of primes. In this work, we formalize these constructions in the Mizar system. We focus on the set of prime numbers and its explicit representation using 10 variables. It is the smallest representation known today. For this, we show that the exponential function is diophantine, together with the same properties for the binomial coefficient and factorial. This formalization is the next step in the research on formal approaches to diophantine sets following the DPRM theorem.
BibTex
@inproceedings{zgjjckmojpju-itp22, author = {Zar Goerzel and Jan Jakubuv and Cezary Kaliszyk and Mirek Olsak and Jelle Piepenbroek and Josef Urban}, booktitle = {13th International Conference on Interactive Theorem Proving, {ITP} 2022}, doi = {10.4230/LIPIcs.ITP.2022.16}, editor = {June Andronick and Leonardo de Moura}, pages = {16:1--16:21}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, series = {LIPIcs}, title = {The Isabelle Enigma}, url = {https://doi.org/10.4230/LIPIcs.ITP.2022.16}, volume = {237}, year = {2022}}
- Details
- Category: Publications 2022
Zar Goerzel, Jan Jakubův, Cezary Kaliszyk, Mirek Olšák, Jelle Piepenbroek, Josef Urban
13th International Conference on Interactive Theorem Proving, ITP 2022, pp. 16:1—16:21, 2022.
pdf doi:10.4230/LIPIcs.ITP.2022.16
Abstract
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.
BibTex
@inproceedings{zgjjckmojpju-itp22, author = {Zar Goerzel and Jan Jakubuv and Cezary Kaliszyk and Mirek Olsak and Jelle Piepenbroek and Josef Urban}, booktitle = {13th International Conference on Interactive Theorem Proving, {ITP} 2022}, doi = {10.4230/LIPIcs.ITP.2022.16}, editor = {June Andronick and Leonardo de Moura}, pages = {16:1--16:21}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, series = {LIPIcs}, title = {The Isabelle Enigma}, url = {https://doi.org/10.4230/LIPIcs.ITP.2022.16}, volume = {237}, year = {2022}}
- Details
- Category: Publications 2022
Grzegorz Prusak, Cezary Kaliszyk
Proceedings of the Workshop on Practical Aspects of Automated Reasoning, PAAR 2022, 2022.
Abstract
Tableaux-based provers work well for certain classes of first-order formulas and are better suited for integration with machine learning techniques. However, the tableaux techniques developed so far perform way worse than saturation-based techniques on the first-order formulas with equality. In this paper, we present the first implementation of Lazy Paramodulation which allows applying the ordering constraints in connection tableaux proof search without exponential blowup of the number of clauses (characteristic for Brand’s modifications). We implement the original Lazy Paramodulation calculus and propose a variant of the Brand’s modification (called LP-modification), which is based on the same ideas as Lazy Paramodulation, avoids exponential blowup and is just a preprocessing step for the standard Connection Tableaux calculus. We demonstrate the impact of both the Lazy Paramodulation and LP-modification on the proof search on a benchmark of TPTP library problems.
BibTex
@inproceedings{gpck-paar22, author = {Grzegorz Prusak and Cezary Kaliszyk}, booktitle = {Proceedings of the Workshop on Practical Aspects of Automated Reasoning, PAAR 2022}, editor = {Boris Konev and Claudia Schon and Alexander Steen}, publisher = {CEUR-WS.org}, series = {{CEUR} Workshop Proceedings}, title = {Lazy Paramodulation in Practice}, url = {http://ceur-ws.org/Vol-3201/paper3.pdf}, volume = {3201}, year = {2022}}
- Details
- Category: Publications 2022
Ujkan Sulejmani, Manuel Eberl, Katharina Kreuzer
Archive of Formal Proofs 2022.
Abstract
This article is a formalisation of a proof of the Hales-Jewett theorem presented in the textbook Ramsey Theory by Graham et al. The Hales-Jewett theorem is a result in Ramsey Theory which states that, for any non-negative integers r and t, there exists a minimal dimension N, such that any r-coloured N’-dimensional cube over t elements (with N’ >= N) contains a monochromatic line. This theorem generalises Van der Waerden’s Theorem, which has already been formalised in another AFP entry.
BibTex
@article{Hales_Jewett-AFP, author = {Ujkan Sulejmani and Manuel Eberl and Katharina Kreuzer}, title = {The {H}ales–{J}ewett Theorem}, journal = {Archive of Formal Proofs}, month = {September}, year = {2022}, note = {\url{https://isa-afp.org/entries/Hales_Jewett.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
4th International Workshop on Formal Methods for Blockchains, FMBC 2022, pp. 4:1-4:15, 2022.
pdf doi:10.4230/OASIcs.FMBC.2022.4
Abstract
Proofgold is a peer to peer cryptocurrency making use of formal logic. Users can publish theories and then develop a theory by publishing documents with definitions, conjectures and proofs. The blockchain records the theories and their state of development (e.g., which theorems have been proven and when). Two of the main theories are a form of classical set theory (for formalizing mathematics) and an intuitionistic theory of higher-order abstract syntax (for reasoning about syntax with binders). We have also significantly modified the open source Proofgold Core client software to create a faster, more stable and more efficient client, Proofgold Lava. Two important changes are the cryptography code and the database code, and we discuss these improvements. We also discuss how the Proofgold network can be used to support large formalization efforts.
BibTex
@inproceedings{cbcktgju-fmbc22, author = {Chad E. Brown and Cezary Kaliszyk and Thibault Gauthier and Josef Urban}, booktitle = {4th International Workshop on Formal Methods for Blockchains, FMBC 2022}, doi = {10.4230/OASIcs.FMBC.2022.4}, editor = {Zaynah Dargaye and Clara Schneidewind}, pages = {4:1--4:15}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, series = {OASIcs}, title = {Proofgold: Blockchain for Formal Methods}, url = {https://doi.org/10.4230/OASIcs.FMBC.2022.4}, volume = {105}, year = {2022}}
- Details
- Category: Publications 2022
Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel, Patrick Lederer
Archive of Formal Proofs 2022.
pdf doi:10.1609/aaai.v37i5.25694 AFP entry
Abstract
In party-approval multi-winner elections, the goal is to allocate the seats of a fixed-size committee to parties based on approval ballots of the voters over the parties. In particular, each can approve multiple parties and each party can be assigned multiple seats.
Three central requirements in this settings are:
Anonymity: The result is invariant under renaming the voters.
Representation:Every sufficiently large group of voters with similar preferences is represented by some committee members.
Strategy-proofness: No voter can benefit by misreporting her true preferences.
We show that these three basic axioms are incompatible for party-approval multi-winner voting rules, thus proving a far-reaching impossibility theorem. The proof of this result is obtained by formulating the problem in propositional logic and then letting a SAT solver show that the formula is unsatisfiable. The DRUP proof output by the SAT solver is then converted into Lammich’s GRAT format and imported into Isabelle/HOL with some custom-written ML code.This transformation is proof-producing, so the final Isabelle/HOL theorem does not rely on any oracles or other trusted external trusted components.
BibTex
@article{PAPP_Impossibility-AFP, author = {Théo Delemazure and Tom Demeulemeester and Manuel Eberl and Jonas Israel and Patrick Lederer}, title = {The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections}, journal = {Archive of Formal Proofs}, month = {November}, year = {2022}, note = {\url{https://isa-afp.org/entries/PAPP_Impossibility.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2022