Publications in 2021
Regular Tree Relations
Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel
Archive of Formal Proofs 2021.
Factorization of Polynomials with Algebraic Coefficients
Manuel Eberl, René Thiemann
Archive of Formal Proofs 2021.
A Formalization of Weighted Path Orders and Recursive Path Orders
Christian Sternagel, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2021.
Fast and Slow Enigmas and Parental Guidance
Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubův, Miroslav Olšák, Josef Urban
Frontiers of Combining Systems (FroCoS),
Lecture Notes in Computer Science 12941,
pp. 173 - 191,
2021.
Learning Theorem Proving Components
Karel Chvalovský, Jan Jakubův, Miroslav Olšák, Josef Urban
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX),
Lecture Notes in Computer Science 12842,
pp. 266 - 278,
2021.
Solving Cubic and Quartic Equations
René Thiemann
Archive of Formal Proofs 2021.
JEFL: Joint Embedding of Formal Proof Libraries
Qingxiang Wang, Cezary Kaliszyk
Frontiers of Combining Systems – 13th International Symposium, FroCoS 2021,
pp. 154-170,
2021.
Towards Finding Longer Proofs
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021),
pp. 167-186,
2021.
Machine Learning Guidance for Connection Tableaux
Michael Färber, Cezary Kaliszyk, Josef Urban
Journal of Automated Reasoning 65,
pp. 287 - 320,
2021.
TacticToe: Learning to Prove with Tactics
Thibault Gauthier,Cezary Kaliszyk,Josef Urban,Ramana Kumar,Michael Norrish
Journal of Automated Reasoning 65,
pp. 257 - 286,
2021.
Multi-redexes and multi-treks induce residual systems; least upper bounds and left-cancellation up to homotopy
Vincent van Oostrom
10th International Workshop on Confluence (IWC 2021),
pp. 7,
2021.
Formalized Signature Extension Results for Confluence, Commutation and Unique Normal Forms
Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 10th International Workshop on Confluence (IWC 2021),
pp. 25 - 30,
2021.
Online Machine Learning Techniques for Coq: A Comparison
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Intelligent Computer Mathematics – 14th International Conference, CICM 2021,
pp. 67-83,
2021.
Characteristic Subsets of SMT-LIB Benchmarks
Jan Jakubův, Mikoláš Janota, Andrew Reynolds
International Workshop on Satisfiability Modulo Theories (SMT),
CEUR Workshop Proceedings 2908,
2021.
Polynomial Termination over N is Undecidable
Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 17th International Workshop on Termination (WST 2021),
pp. 21 - 26,
2021.
GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry
Miroslav Olšák
International Congress on Mathematical Software (ICMS 2020),
pp. 263 - 271,
2020.
Z; Syntax-Free Developments
Vincent van Oostrom
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021),
Leibniz International Proceedings in Informatics (LIPIcs) 195,
pp. 24:1 - 24:22,
2021.
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, Josef Urban
International Joint Conference on Automated Reasoning (IJCAR),
pp. 448 - 463,
2020.
A Perron–Frobenius theorem for deciding matrix growth
René Thiemann
Journal of Logical and Algebraic Methods in Programming 123,
2021.
Artificial Intelligence and Domain-Specific Languages for Interactive Theorem Proving
Yutaka Nagashima
PhD thesis, University of Innsbruck 2021.
CoCo 2019: Report on the Eighth Confluence Competition
Aart Middeldorp, Julian Nagele, Kiraku Shintani
International Journal on Software Tools for Technology Transfer 23,
pp. 905 - 916,
2021.
Certifying Proofs in the First-Order Theory of Rewriting
Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer
27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021),
LNCS 12652,
pp. 127 – 144,
2021.
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
Ralph Bottesch, Jose Divasón, René Thiemann
Archive of Formal Proofs 2021.
The Sunflower Lemma of Erdős and Rado
René Thiemann
Archive of Formal Proofs 2021.
A study of continuous vector representations for theorem proving
Stanisław Purgał, Julian Parsert, Cezary Kaliszyk
Journal of Logic and Computation
pp. 27,
2021.
Maltsev conditions for general congruence meet-semidistributive algebras
Miroslav Olšák
The Journal of Symbolic Logic
pp. 20,
2021.
An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR
Max Haslbeck, Rene Thiemann
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),
pp. 238 – 249,
2021.
A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer
10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),
pp. 250 – 263,
2021.
Disambiguating Symbolic Expressions in Informal Documents
Dennis Müller and Cezary Kaliszyk
International Conference on Learning Representations (ICLR),
pp. 16,
2021.