Publications in 2020
Property Invariant Embedding for Automated Reasoning
Miroslav Olšák, Cezary Kaliszyk, Josef Urban
24th European Conference on Artificial Intelligence (ECAI 2020),
Frontiers in Artificial Intelligence and Applications 325,
pp. 1395 – 1402,
2020.
Maximal Non-compactness of Sobolev Embeddings
Jan Lang, Vít Musil, Miroslav Olšák, Luboš Pick
The Journal of Geometric Analysis 31,
pp. 9406 - 9431,
2020.
Improving Expressivity of Graph Neural Networks
Stanisław Purgał
International Joint Conference on Neural Networks (IJCNN),
pp. 1 – 7,
2020.
A Survey of Languages for Formalizing Mathematics
Cezary Kaliszyk, Florian Rabe
Intelligent Computer Mathematics (CICM 2020),
LNCS 12236,
pp. 138 – 156,
2020.
Some symmetries of commutation diamonds
Vincent van Oostrom
9th International Workshop on Confluence,
pp. 1 – 5,
2020.
Some symmetries of commutation diamonds
Vincent van Oostrom
9th International Workshop on Confluence (IWC 2020),
pp. 5,
2020.
Certifying the Weighted Path Order
Rene Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020),
Leibniz International Proceedings in Informatics (LIPIcs) 167,
pp. 4:1 – 4:20,
2020.
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL
René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J.C. Joosten, Akihisa Yamada
Journal of Automated Reasoning 64,
pp. 827 – 856,
2020.
A Formalization of Knuth-Bendix Orders
Christian Sternagel, René Thiemann
Archive of Formal Proofs 2020.
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL
Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann
12th International NASA Formal Methods Symposium (NFM 2020),
LNCS 12229,
pp. 233 – 250,
2020.
Property Preserving Embedding of First-order Logic
Julian Parsert, Stephanie Autherith, Cezary Kaliszyk
6th Global Conference on Artificial Intelligence (GCAI 2020),
EPiC Series in Computing 72,
pp. 70 – 82,
2020.
Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
Alexander Lochmann, Aart Middeldorp
26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,
LCNS 12079,
pp. 25 – 40,
2020.
Relaxed Weighted Path Order in Theorem Proving
Jan Jakubův, Cezary Kaliszyk
Mathematics in Computer Science,
14,
pp. 657 – 670,
2020.
Tools in Term Rewriting for Education
Sarah Winker, Aart Middeldorp
8th International Workshop on Theorem Proving Components for Educational Software,
EPTCS 313,
pp. 54 – 72,
2020.
The local loop lemma
Miroslav Olšák
Algebra universalis 81,
pp. 23,
2020.
Verified Analysis of Random Binary Tree Structures
Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Journal of Automated Reasoning 64,
pp. 879 – 910,
2020.
Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq
Burak Ekici, Cezary Kaliszyk
Mathematics in Computer Science,
14,
pp. 533 – 549,
2020.
Exploration of neural machine translation in autoformalization of mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, Josef Urban
International Conference on Certified Programs and Proofs (CPP 2020),
ACM
pp. 85 – 98,
2020.