General Information

Name
Teppei SAITO
齊藤 哲平
Research Interests
term rewriting
automated theorem proving
Affiliation
JAIST
E-mail Address
saito@jaist.ac.jp
Activities
CoCo Steering Committee (from 2022)
Software
Toma
IsaFoR/CeTA (as a contributor)

Conference Papers

CADE 2025
Teppei Saito and Nao Hirokawa.
Lexicographic Combination of Reduction Pairs.
Proceedings of the 30th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence (to appear).
submitted version
extended version available upon request
CPP 2025
Dohan Kim, Teppei Saito, René Thiemann and Akihisa Yamada.
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting.
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 272–282 2025.
doi: 10.1145/3703595.3705889
prototoype tool
errata

In Example 6.2: AN(x,y) = x should read AN(x,y) = y.

FSCD 2024
Teppei Saito and Nao Hirokawa.
Simulating Dependency Pairs by Semantic Labeling.
Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 299, pp. 13:1–13:20 2024.
doi: 10.4230/LIPICS.FSCD.2024.13
FroCoS 2023
Teppei Saito and Nao Hirokawa.
Weighted Path Orders are Semantic Path Orders.
Proceedings of the 14th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 14279, pp. 63–80, 2023.
doi: 10.1007/978-3-031-43369-6_4
best paper award
errata

Before Lemma 2: T≤M should read SN(>spo)≤M.

Proposition 5: polynomials in G and H must be of the form c x + d for some c ∈ {0, 1} and integer d. In addition, what is called linear polynomial over natural numbers in the surrounding text mean polynomials of this form.

Links