Publications in 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.

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.

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.

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 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.

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.