Titlebook: Rewriting Techniques and Applications; 9th International Co Tobias Nipkow Conference proceedings 1998 Springer-Verlag Berlin Heidelberg 199

NIP

978-3-540-64301-2Springer-Verlag Berlin Heidelberg 1998

parallelism

ligature

glamor

https://doi.org/10.1007/BFb0052355Algorithms; Automat; Constraint; Monoid; Rack; Resolution; Variable; algorithm; functional programming; lambd

确定

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.

平静生活

conscribe

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

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.

繁忙

-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