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.

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.

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.

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 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.