Affection
发表于 2025-3-30 09:51:28
A case study of completion modulo distributivity and Abelian groups, exist canonical rewrite systems for these theories. As a test case of our approach, we show how to build the free Abelian groups and distributivity laws in the completion procedure. The empirical results of our experiment on proving many identities in alternative rings show clearly that the gain of
收养
发表于 2025-3-30 13:50:33
A semantic approach to order-sorted rewriting,order-sorted rewriting the term rewriting system needs to be sort decreasing in order to be able to prove a critical pair lemma and Birkhoff‘s completeness theorem. However, this approach is too restrictive..Therefore, we generalize well-sorted terms to semantically well-sorted terms and well-sorted
河流
发表于 2025-3-30 18:10:18
http://reply.papertrans.cn/83/8300/829952/829952_53.png
羊栏
发表于 2025-3-30 23:30:10
http://reply.papertrans.cn/83/8300/829952/829952_54.png
NOVA
发表于 2025-3-31 01:12:18
http://reply.papertrans.cn/83/8300/829952/829952_55.png
阻挠
发表于 2025-3-31 06:52:01
Equational and membership constraints for infinite trees, and entailment tests and is therefore suitable for the use in concurrent constraint programming systems which are based on cyclic data structures..Our set defining devices are greatest . of regular systems of equations with a deterministic form of union. As the main technical particularity of the a
可商量
发表于 2025-3-31 10:51:15
Proving properties of typed lambda terms: Realizability, covers, and sheaves,ich uses the notion of a cover algebra (as in abstract sheaf theory). For this, we introduce a new class of semantic structures equipped with preorders, called preapplicative structures. In this framework, a general realizability theorem can be shown. Applying this theorem to the special case of the
轻快带来危险
发表于 2025-3-31 16:55:22
Some lambda calculi with categorical sums and products,rd equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latte
影响深远
发表于 2025-3-31 17:41:55
,Paths, computations and labels in the λ-calculus, that redexes in a same family are created by “contraction” (via .-reduction) of a unique common path in the initial term. This fact gives new evidence about the “common nature” of redexes in a same family, and about the possibility of sharing their reduction. From this point of view, our characteri
暗语
发表于 2025-3-31 22:32:10
Confluence and superdevelopments, the orthogonal combinatory reduction systems. Combinatory reduction systems (CRSs for short) were introduced by Klop generalizing an idea of Aczel. In CRSs, the usual first-order term rewriting format is extended with binding structures for variables. This permits to express besides first order ter