NIP
发表于 2025-3-23 12:57:52
978-3-540-64301-2Springer-Verlag Berlin Heidelberg 1998
parallelism
发表于 2025-3-23 15:56:49
http://reply.papertrans.cn/83/8300/829963/829963_12.png
ligature
发表于 2025-3-23 18:06:58
http://reply.papertrans.cn/83/8300/829963/829963_13.png
glamor
发表于 2025-3-24 01:50:16
https://doi.org/10.1007/BFb0052355Algorithms; Automat; Constraint; Monoid; Rack; Resolution; Variable; algorithm; functional programming; lambd
确定
发表于 2025-3-24 06:23:09
Normalization of S-terms is decidable,The combinator S has the reduction rule . . (.). We investigate properties of ground terms built from S alone. We show that it is decidable whether such an .-term has a normal form. The decision procedure makes use of rational tree languages. We also exemplify and summarize other properties of .-terms and hint at open questions.
平静生活
发表于 2025-3-24 09:48:29
http://reply.papertrans.cn/83/8300/829963/829963_16.png
conscribe
发表于 2025-3-24 13:49:29
Simultaneous critical pairs and Church-Rosser property,y left-linear term rewriting systems. Our result extends the well-known criterion given by Huet (1980), Toyama (1988), and Oostrom (1997) and incomparable with other well-known criteria for left-linear systems.
Conduit
发表于 2025-3-24 18:06:59
Church-Rosser theorems for abstract reduction modulo an equivalence relation,hnique is extended in two ways to abstract rewriting modulo an equivalence relation. It is shown that known Church-Rosser theorems can be viewed as special cases of the new criteria. Moreover, applications of the new criteria yield several new results.
繁忙
发表于 2025-3-24 21:19:08
-unification for subsystems of ,al modal logics . and .. It presents improved unification algorithms for certain forms of the right identity and associativity laws. The algorithms employ mutation rules, which have the advantage that terms are worked off from the outside inward, making paramodulating into terms superfluous.
MAPLE
发表于 2025-3-25 00:51:42
http://reply.papertrans.cn/83/8300/829963/829963_20.png