Publications in 2018

A Verified Implementation of Algebraic Numbers in Isabelle/HOL
Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Journal of Automated Reasoning 64, pp. 363 – 389, 2020.

Reinforcement Learning of Theorem Proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
Advances in Neural Information Processing Systems,  31, pp. 8836 – 8847, 2018.

Learning Proof Search in Proof Assistants
Michael Färber
PhD thesis, University of Innsbruck, 2018.

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
Ralph Bottesch, Max W. Haslbeck, René Thiemann
22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, EPiC Series in Computing 57, pp. 164 – 180, 2018.

Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently
Bertram Felgenhauer
Logical Methods in Computer Science 14(4:7), pp. 1 – 35, 2018.

IMP with Exceptions over Decorated Logic
Burak Ekici
Discrete Mathematics and Theoretical Computer Science 20(2), pp. 1 – 43, 2018.

Layer Systems for Confluence — Formalized
Bertram Felgenhauer and Franziska Rapp
Proceedings of the 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018), Lecture Notes in Computer Science 11187, pp. 173 – 190, 2018.

Semantics of Mizar as an Isabelle Object Logic
Cezary Kaliszyk, Karol Pąk
Journal of Automated Reasoning  pp. 1 – 39, 2018.

On W[1]-Hardness as Evidence for Intractability
Ralph C. Bottesch
43rd International Symposium on Mathematical Foundations of Computer Science, Leibniz International Proceedings in Informatics 117, pp. 73:1 – 73:15, 2018.

An Incremental Simplex Algorithm with Unsatisfiable Core Generation
Filip Marić, Mirko Spasić, René Thiemann
Archive of Formal Proofs 2018.

Towards Mac Lane’s Comparison Theorem for the (co)Kleisli Construction in Coq
Burak Ekici
4th Workshop on Formal Mathematics for Mathematicians, CEUR Workshop Proceedings,  pp. 1 – 5, 2018.

First Experiments with Neural Translation of Informal to Formal Mathematics
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
11th International Conference on Intelligent Computer Mathematics, LNCS 11006, pp. 255 – 270, 2018.

Isabelle Import Infrastructure for the Mizar Mathematical Library
Cezary Kaliszyk and Karol Pąk
11th International Conference on Intelligent Computer Mathematics, LNCS 11006, pp. 131 – 146, 2018.

MaedMax: A Maximal Ordered Completion Tool
Sarah Winkler, Georg Moser
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 472 – 480, 2018.

Towards a Unified Ordering for Superposition-Based Automated Reasoning
Jan Jakubův, Cezary Kaliszyk
6th International Conference on Mathematical Software, Lecture Notes in Computer Science 10931, pp. 245 – 254, 2018.

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

ProTeM: A Proof Term Manipulator (System Description)
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.

Completion for Logically Constrained Rewriting
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.

Towards Formal Foundations for Game Theory
Julian Parsert, Cezary Kaliszyk
Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 495 – 503, 2018.

A Formalization of the LLL Basis Reduction Algorithm
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.

CoCo 2018 Participant: CSI 1.2.1
Bertram Felgenhauer, Aart Middeldorp, Fabian Mitterwallner, and Julian Nagele
Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 76, 2018.

A Formally Verified Solver for Homogeneous Linear Diophantine Equations
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.

Cops and CoCoWeb: Infrastructure for Confluence Tools
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.

FORT 2.0
Franziska Rapp, Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 81 – 88, 2018.

Aligning Concepts across Proof Assistant Libraries
Thibault Gauthier, Cezary Kaliszyk
J. Symbolic Computation 90, pp. 89 – 123, 2018.

Learning-Assisted Reasoning within Proof Assistants
Thibault Gauthier
PhD thesis, University of Innsbruck,  2018.

Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order Rewrite Systems
Julian Nagele
PhD thesis, University of Innsbruck, 2017.

Elementary equivalence in Artin groups of finite type
Arpan Kabira, T. V. H. Prathamesh, Rishi Vyas
International Journal of Algebra and Computation 28, pp. 331-344, 2018.

Hammer for Coq: Automation for Dependent Type Theory
Łukasz Czajka, Cezary Kaliszyk
J. Autom. Reasoning 61, pp. 423 – 453, 2018.

A verified factorization algorithm for integer polynomials with polynomial complexity
Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2018.

A verified LLL algorithm
Ralph Bottesch, Jose Divasón, Max Haslbeck, Sebastiaan Joosten, René Thiemann, Akihisa Yamada
Archive of Formal Proofs 2018.

First-Order Terms
Christian Sternagel, René Thiemann
Archive of Formal Proofs,  2018.

Efficient Certification of Complexity Proofs – Formalizing the Perron-Frobenius Theorem
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.

Formal Microeconomic Foundations and the First Welfare Theorem
Julian Parsert, Cezary Kaliszyk
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018),   pp. 91-101, 2018.