Search

Your search keyword '"reduction order"' showing total 4 results
Start Over Descriptor "reduction order" Search Limiters Full Text
4 results on '"reduction order"'

1. 依存対手法の簡約順序への再定式化

Author

Guo, Ziyu

Subjects
項書換え, 簡約順序, Reduction Order, 依存対手法, Dependency Pair Method, Term Rewriting
Abstract

Supervisor: 廣川 直, 先端科学技術研究科, 修士(情報科学)

Published
2023

2. Completion and Reduction Orders (Invited Talk)

Author

Nao Hirokawa, Hirokawa, Nao, Nao Hirokawa, and Hirokawa, Nao

Abstract

We present three techniques for improving the Knuth-Bendix completion procedure and its variants: An order extension by semantic labeling, a new confluence criterion for terminating term rewrite systems, and inter-reduction for maximal completion.

Published
2021
Full Text
View/download PDF

3. A unified ordering for termination proving.

Author

Yamada, Akihisa, Kusakari, Keiichirou, and Sakabe, Toshiki

Subjects
*MALWARE, *POLYNOMIALS, *LEXICOGRAPHY, *SOFTWARE frameworks, *DATA analysis
Abstract

We introduce a reduction order called the weighted path order (WPO) that subsumes many existing reduction orders. WPO compares weights of terms as in the Knuth–Bendix order (KBO), while WPO allows weights to be computed by a wide class of interpretations. We investigate summations, polynomials and maximums for such interpretations. We show that KBO is a restricted case of WPO induced by summations, the polynomial order (POLO) is subsumed by WPO induced by polynomials, and the lexicographic path order (LPO) is a restricted case of WPO induced by maximums. By combining these interpretations, we obtain an instance of WPO that unifies KBO, LPO and POLO. In order to fit WPO in the modern dependency pair framework, we further provide a reduction pair based on WPO and partial statuses. As a reduction pair, WPO also subsumes matrix interpretations. We finally present SMT encodings of our techniques, and demonstrate the significance of our work through experiments. [ABSTRACT FROM AUTHOR]

Published
2015
Full Text
View/download PDF

4. Certifying the Weighted Path Order (Invited Talk)

Author

René Thiemann and Jonas Schöpf and Christian Sternagel and Akihisa Yamada, Thiemann, René, Schöpf, Jonas, Sternagel, Christian, Yamada, Akihisa, René Thiemann and Jonas Schöpf and Christian Sternagel and Akihisa Yamada, Thiemann, René, Schöpf, Jonas, Sternagel, Christian, and Yamada, Akihisa

Abstract

The weighted path order (WPO) unifies and extends several termination proving techniques that are known in term rewriting. Consequently, the first tool implementing WPO could prove termination of rewrite systems for which all previous tools failed. However, we should not blindly trust such results, since there might be problems with the implementation or the paper proof of WPO. In this work, we increase the reliability of these automatically generated proofs. To this end, we first formally prove the properties of WPO in Isabelle/HOL, and then develop a verified algorithm to certify termination proofs that are generated by tools using WPO. We also include support for max-polynomial interpretations, an important ingredient in WPO. Here we establish a connection to an existing verified SMT solver. Moreover, we extend the termination tools NaTT and TTT2, so that they can now generate certifiable WPO proofs.

Published
2020
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results