All Publications


Some symmetries of commutation diamonds
Vincent van Oostrom
9th International Workshop on Confluence, pp. 1 – 5, 2020.
  PDF
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.
  PDF
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.
  PDF
© The Author(s) 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.
  PDF
Verified Analysis of Random Binary Tree Structures
Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Journal of Automated Reasoning 64, pp. 879 – 910, 2020.
  PDF
Loop conditions for strongly connected digraphs
Miroslav Olšák
International Journal of Algebra and Computation pp. 1 – 33, 2019.
  PDF
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.
  PDF
Declarative Proof Translation
Cezary Kaliszyk, Karol Pąk
10th International Conference on Interactive Theorem Proving, LIPIcs 141, pp. 35:1 – 35:7, 2019.
  PDF
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.
  PDF 
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.
  PDF
© Springer Nature Switzerland AG 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.
  PDF
Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Logical Methods in Computer Science, 15(3), pp. 19:1 – 19:42, 2019.
  PDF
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.
  PDF
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.
  PDF
© Creative Commons License – CC BY 4.0
Nach oben scrollen