Publications in 2019
Loop conditions for strongly connected digraphs
Miroslav Olšák
International Journal of Algebra and Computation
pp. 1 – 33,
2019.
Higher-order Tarski Grothendieck as a Foundation for Formal Proof
Chad Brown, Cezary Kaliszyk, Karol Pąk
10th International Conference on Interactive Theorem Proving,
LIPIcs 141,
pp. 9:1 – 9:16,
2019.
Declarative Proof Translation
Cezary Kaliszyk, Karol Pąk
10th International Conference on Interactive Theorem Proving,
LIPIcs 141,
pp. 35:1 – 35:7,
2019.
Certification of Nonclausal Connection Tableaux Proofs
Michael Färber, Cezary Kaliszyk
28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,
LNCS 11714,
pp. 21 – 38,
2019.
Confluence by Critical Pair Analysis Revisited
Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi
27th International Conference on Automated Deduction,
Lecture Notes in Computer Science 11716,
pp. 319 – 336,
2019.
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
6th Workshop on Proof eXchange for Theorem Proving,
EPTCS 301,
pp. 18 – 26,
2019.
Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Logical Methods in Computer Science,
15(3),
pp. 19:1 – 19:42,
2019.
Certified Equational Reasoning via Ordered Completion
Christian Sternagel and Sarah Winkler
27th International Conference on Automated Deduction,
Lecture Notes in Computer Science 11716,
pp. 508 – 525,
2019.
GRUNGE: A Grand Unified ATP Challenge
Chad Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
27th International Conference on Automated Deduction,
LNCS 11716,
pp. 123 – 141,
2019.
Composing Proof Terms
Christina Kohl and Aart Middeldorp
27th International Conference on Automated Deduction,
Lecture Notes in Artificial Intelligence 11716,
pp. 337 – 353,
2019.
Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL
Ralph Bottesch, Max W. Haslbeck, and René Thiemann
International Symposium on Frontiers of Combining Systems,
Lecture Notes in Computer Science 11715,
pp. 223 – 239,
2019.
Linear Inequalities
Ralph Bottesch, Alban Reynaud, René Thiemann
Archive of Formal Proofs 2019.
A Verified Implementation of the Berlekamp—Zassenhaus Factorization Algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada
Journal of Automated Reasoning 64(4),
pp. 699 – 735,
2020.
Can Neural Networks Learn Symbolic Rewriting?
Bartosz Piotrowski, Josef Urban, Chad Brown, Cezary Kaliszyk
Learning and Reasoning with Graph-Structured Representations, ICML 2019 Workshop,
2019.
Reachability Analysis for Termination and Confluence of Rewriting
Christian Sternagel, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Lecture Notes in Computer Science 11427,
pp. 262 – 278,
2019.
The Termination and Complexity Competition
Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Lecture Notes in Computer Science 11429,
pp. 155 – 166,
2019.
nonreach – A Tool for Nonreachability Analysis
Florian Meßner, Christian Sternagel
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,
Lecture Notes in Computer Science 11427,
pp. 337 – 343,
2019.
Confluence Competition 2019
Aart Middeldorp, Julian Nagele, and Kiraku Shintani
Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019, part III),
Lecture Notes in Computer Science 11429,
pp. 25 – 40,
2019.
A Hierarchy of Polynomial Kernels
Jouke Witteveen, Ralph Bottesch, Leen Torenvliet
45th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2019),
Lecture Notes in Computer Science 11376,
pp. 504 – 518,
2019.
Farkas’ Lemma and Motzkin’s Transposition Theorem
Ralph Bottesch, Max W. Haslbeck, René Thiemann
Archive of Formal Proofs 2019.
Certified ACKBO
Alexander Lochmann, Christian Sternagel
8th ACM SIGPLAN International Conference on Certified Programs and Proofs,
pp. 144 – 151,
2019.
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
8th ACM SIGPLAN International Conference on Certified Programs and Proofs,
pp. 132 – 143,
2019.