ARI: Automation of Rewriting Infrastructure

ARI is a joint FWF/JSPS project. It will start on 1 July 2022 and run for three years. Further details can be found here.

Members

-

FWF project number

Contact

Publications

Automated Analysis of Logically Constrained Rewrite Systems using crest
Jonas Schöpf, Aart Middeldorp
Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025), Lecture Notes in Computer Science 15696, pp. 124-144, 2025.

Congruence Closure Modulo Groups
Dohan Kim
Logical Methods in Computer Science 2025.

An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025),  2025.

Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Christina Kirk, Aart Middeldorp
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025),   pp. 156-170, 2025.

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.

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.

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.

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.

Confluence Criteria for Logically Constrained Rewrite Systems
Jonas Schöpf, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 474-490, 2023.

A New Format for Rewrite Systems
Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, René Thiemann, Akihisa Yamada
12th International Workshop on Confluence (IWC),   pp. 32-37, 2023.

Formalizing Almost Development Closed Critical Pairs
Christina Kohl, Aart Middeldorp
Proceedings of the 14th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics 268, pp. 38:1-38:8, 2023.

A Verified Efficient Implementation of the Weighted Path Order
René Thiemann, Elias Wenninger
Archive of Formal Proofs 2023.

A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl, Aart Middeldorp
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023),   pp. 197-210, 2023.