Publications in 2017

Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
Cezary Kaliszyk, Karol Pąk
International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2017), Lecture Notes in Computer Science 10693, pp. 163 – 178, 2017.

Reliable Confluence Analysis of Conditional Term Rewrite Systems
Thomas Sternagel
PhD thesis, University of Innsbruck, 2017.

System Description: Statistical Parsing of Informalized Mizar Formulas
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, IEEE Computer Society  pp. 169 – 172, 2017.

Stochastic Matrices and the Perron-Frobenius Theorem
René Thiemann
Archive of Formal Proofs 2017.

Constructing Cycles in the Simplex Method for DPLL(T)
Bertram Felgenhauer and Aart Middeldorp
Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC 2017), Lecture Notes in Computer Science 10580, pp. 213 – 228, 2017.

CoCo 2017 Participant: FORT 1.0
Franziska Rapp and Aart Middeldorp
Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 78, 2017.

CoCo 2017 Participant: CSI 1.1
Bertram Felgenhauer, Aart Middeldorp, and Julian Nagele
Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 76, 2017.

Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, and Christian Sternagel
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics 84, pp. 19:1 – 19:16, 2017.

Progress in the Independent Certification of Mizar Mathematical Library in Isabelle
Cezary Kaliszyk and Karol Pąk
Federated Conference on Computer Science and Information Systems (2017), Annals of Computer Science and Information Systems 11, pp. 227 – 236, 2017.

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
Proceedings of the 14th International Symposium on Frontiers of Combining Systems, LNCS 10483, pp. 3-21, 2017.

Automating Formalization by Statistical and Semantic Parsing of Mathematics
Cezary Kaliszyk, Josef Urban, Jiřı́ Vyskočil
8th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 10499, pp. 12 – 27, 2017.

Certifying Safety and Termination Proofs for Integer Transition Systems
Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
Proceedings of the 26th International Confluence on Automated Deduction, Lecture Notes in Computer Science 10395, pp. 454-471, 2017.

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
Christian Sternagel, Thomas Sternagel
Proceedings of the 26th International Confluence on Automated Deduction, LNCS 10395, pp. 413-431, 2017.

CSI: New Evidence – A Progress Report
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017.

Monte Carlo Tableau Proof Search
Michael Färber, Cezary Kaliszyk, Josef Urban
26th International Conference on Automated Deduction, LNCS 10395, pp. 563-579, 2017.

Classification of Alignments Between Concepts of Formal Mathematical Systems
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 83-98, 2017.

Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
Cezary Kaliszyk and Karol Pąk
10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 193-207, 2017.

Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
ACM Transactions on Computational Logic 18(2), pp. 14:1 – 14:50, 2017.

A formal proof of the Kepler conjecture
THOMAS HALES, MARK ADAMS, GERTRUD BAUER, TAT DAT DANG, JOHN HARRISON, LE TRUONG HOANG, CEZARY KALISZYK, VICTOR MAGRON, SEAN MCLAUGHLIN, TAT THANG NGUYEN, QUANG TRUONG NGUYEN, TOBIAS NIPKOW, STEVEN OBUA, JOSEPH PLESO, JASON RUTE, ALEXEY SOLOVYEV, THI HOAI AN TA, NAM TRUNG TRAN, THI DIEP TRIEU, JOSEF URBAN, KY VU, ROLAND ZUMKELLER
Forum of Mathematics, Pi,  5, pp. 1-29, 2017.

Parsing and Printing of and with Triples
Sebastiaan J. C. Joosten
Relational and Algebraic Methods in Computer Science. RAMICS 2017, Lecture Notes in Computer Science 10226, pp. 159 – 176, 2017.

Certifying Confluence Proofs via Relative Termination and Rule Labeling
Julian Nagele, Bertram Felgenhauer, and Harald Zankl
Logical Methods in Computer Science,  13(2:4), pp. 1 – 27, 2017.

Deep Network Guided Proof Search
Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk.
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC 46, pp. 85-105, 2017.

TacticToe: Learning to Reason with HOL4 Tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPIC 46, pp. 125-143, 2017.

Wikis and Collaborative Systems for Large Formal Mathematics
Cezary Kaliszy, Josef Urban
Post proceedings of Semantic Web Collaborative Spaces, LNCS  pp. 35-52, 2016.

A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Jose Divason, Sebastiaan J. C. Joosten, Rene Thiemann and Akihisa Yamada
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017),   pp. 17 – 29, 2017.

Subresultants
Sebastiaan Joosten and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2017.

Reachability, Confluence, and Termination Analysis with State-Compatible Automata
Bertram Felgenhauer and René Thiemann
Information and Computation 253(3), pp. 467 – 483, 2017.

Towards Formal Proof Metrics
David Aspinall, Cezary Kaliszyk
19th International Conference on Fundamental Approaches to Software Engineering, LNCS 9633, pp. 325-341, 2016.

Relative Termination via Dependency Pairs
José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada
Journal of Automated Reasoning 58(3), pp. 391 – 411, 2017.

Complexity of Conditional Term Rewriting
Cynthia Kop, Aart Middeldorp, Thomas Sternagel
Logical Methods in Computer Science 13(1:6), pp. 1 – 56, 2017.

Analyzing Program Termination and Complexity Automatically with AProVE
Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann
Journal of Automated Reasoning,  58(1), pp. 3 – 31, 2017.