Publications in 2024

Finding k Shortest Paths in Cayley Graphs of Finite Groups
Dohan Kim
Graphs and Combinatorics 2024.

An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility
Dohan Kim
15th International Conference on Interactive Theorem Proving (ITP 2024),  2024.

Guiding Enumerative Program Synthesis with Large Language Models
Yixuan Li, Julian Parsert, Elizabeth Polgreen
Computer Aided Verification – 36th International Conference (CAV), Lecture Notes in Computer Science 14682, pp. 280-301, 2024.

Linear Termination is Undecidable
Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), ACM  pp. 57:1-57:12, 2024.

A Verified Algorithm for Deciding Pattern Completeness
René Thiemann and Akihisa Yamada
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024),   pp. 27:1-27:17, 2024.

Equational Theories and Validity for Logically Constrained Term Rewriting
Takahito Aoto, Naoki Nishida, Jonas Schöpf
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Leibniz International Proceedings in Informatics (LIPIcs) 299, pp. 31:1-31:21, 2024.

Confluence of Logically Constrained Rewrite Systems Revisited
Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Lecture Notes in Artificial Intelligence 14740, pp. 298-316, 2024.

A Preprocessor for Linear Diophantine Equalities and Inequalities
René Thiemann
Archive of Formal Proofs 2024.

Sorted Terms
Akihisa Yamada and René Thiemann
Archive of Formal Proofs 2024.

Verifying a Decision Procedure for Pattern Completeness
René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2024.

Undecidability Results on Orienting Single Rewrite Rules
René Thiemann, Fabian Mitterwallner and Aart Middeldorp
Archive of Formal Proofs 2024.

Equational theorem proving for clauses over strings
Dohan Kim
Mathematical Structures in Computer Science (MSCS) 2024.

Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024),  2024.