Pessary
发表于 2025-3-25 03:39:41
http://reply.papertrans.cn/83/8300/829948/829948_21.png
CHYME
发表于 2025-3-25 08:35:32
Size-Change Termination for Term Rewritingnermost termination of arbitrary term rewrite systems (TRSs). Moreover, we compare this approach with existing techniques for termination analysis of TRSs (such as recursive path orderings or dependency pairs). It turns out that the size-change principle on its own fails for many examples that can b
lethargy
发表于 2025-3-25 12:22:21
Associative-Commutative Rewriting on Large Termsues for converting to and from a more conventional representation together with a heuristic for deciding at runtime when to convert a term to the new representation. We sketch how our approach can be generalized to order-sorted AC rewriting and to other equational theories. We also present some experimental results using the Maude 2 interpreter.
遗忘
发表于 2025-3-25 19:06:48
http://reply.papertrans.cn/83/8300/829948/829948_24.png
Constant
发表于 2025-3-25 20:52:07
Residuals in Higher-Order Rewritingrove that an orthogonal PRS together with the residual operator mentioned above, is a residual system. As a side-effect, all results of (abstract)residual theory are inherited by orthogonal PRSs, such as confluence, and the notion of permutation equivalence of reductions.
miniature
发表于 2025-3-26 02:06:50
New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protoco formalization is an approximation of the set of possible traces, for instance relaxing the nonce freshness assumption. As a consequence, we get some new decidability results for the verification of cryptographic protocols with exclusive or.
finite
发表于 2025-3-26 06:30:04
http://reply.papertrans.cn/83/8300/829948/829948_27.png
暂时过来
发表于 2025-3-26 11:17:13
Efficient Reductions with Director Stringsus offering more sharing). Our experimental results confirm that, for large combinator based terms, our weak evaluation strategies out-perform standard evaluators. Moreover, we derive two abstract machines for strong reduction which inherit the efficiency of the weak evaluators.
政府
发表于 2025-3-26 15:45:54
Two-Way Equational Tree Automata for AC-Like Theories: Decidability and Closure Propertieslled push clauses. (The . case is open.) In particular, the two-way automata modulo these theories are closed under union and intersection, and emptiness is decidable. We also note that alternating variants have undecidable emptiness problem for most theories, contrarily to the non-equational case where alternation is essentially harmless.
机械
发表于 2025-3-26 18:54:11
Size-Change Termination for Term Rewritingfit from their respective advantages, we show how to combine the size-change principle with classical orderings and with dependency pairs. In this way, we obtain a new approach for automated termination proofs of TRSs which is more powerful than previous approaches.