2023-03-22T00:33:59Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:02003931
2023-01-16T04:59:43Z
312:313:314
Transforming orthogonal inductive definition sets into confluent term rewrite systems
Zhang, Shujun
Nishida, Naoki
embargoed access
© 2022. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/
First-order logic
Term rewriting
Program transformation
Inductive theorem
Termination
Dependency pair
In this paper, we transform an orthogonal inductive definition set, which is a set of productions for inductive predicates, into a confluent term rewrite system such that a quantifier-free sequent is valid w.r.t. the inductive definition set if and only if an equation representing the sequent is an inductive theorem of the term rewrite system. To this end, we first propose a transformation of an orthogonal inductive definition set into a confluent term rewrite system that is equivalent to the inductive definition set in the sense of evaluating ground formulas. Then, we show that termination of the inductive definition set is proved by the generalized subterm criterion if and only if termination of the transformed term rewrite system is so. Finally, we show that the transformed term rewrite system with some rewrite rules for sequents has the expected property. In addition, we show a termination criterion for the union of term rewrite systems whose termination is proved by the generalized subterm criterion.
Elsevier
2024-06-01
2022-06
eng
journal article
AM
http://hdl.handle.net/2237/0002003931
https://nagoya.repo.nii.ac.jp/records/2003931
https://doi.org/10.1016/j.jlamp.2022.100779
2352-2208
Journal of Logical and Algebraic Methods in Programming
127
100779
https://nagoya.repo.nii.ac.jp/record/2003931/files/ZhangNishida2022jlamp_preprint.pdf
application/pdf
738 KB
2024-06-01