2023-03-24T12:26:01Z
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
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.
journal article
Elsevier
2022-06
application/pdf
Journal of Logical and Algebraic Methods in Programming
127
100779
2352-2208
https://nagoya.repo.nii.ac.jp/record/2003931/files/ZhangNishida2022jlamp_preprint.pdf
eng
https://doi.org/10.1016/j.jlamp.2022.100779
© 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/