Salvador Lucas

We consider sets/relations/computations defined by Elementary Inference Systems I , which are obtained from Smullyan's elementary formal systems using Gentzen's notation for inference rules, and proof trees for atoms P(t 1 ,. .. ,t n), where predicate P represents the considered set/relation/computation. A first-order theory Th(I), actually a set of definite Horn clauses, is given to I. Properties of objects defined by I are expressed as first-order sentences F, which are proved true or false by satisfaction M |= F of F in a canonical model M of Th(I). For this reason, we call F a semantic property of I. Since canonical models are, in general, incomputable, we show how to (dis)prove semantic properties by satisfiability in an arbitrary model A of Th(I). We apply these ideas to the analysis of properties of programming languages and systems whose computations can be described by means of an elementary inference system. In particular, rewriting-based systems.

Generalized Term Rewriting Systems (GTRSs) extend Conditional Term Rewriting Systems by (i) selecting the arguments of function symbols on which rewritings are allowed and (ii) allowing for more general conditions in rules, namely, atoms defined by a set of Horn clauses. They are useful to model and analyze properties of computations with sophisticated languages like . Toyama proved that left-linear and almost parallel-closed Term Rewriting Systems (TRSs) are confluent. In this paper, we generalize and extend his result to GTRSs without requiring left-linearity . This improves Toyama’s result, as we show with some examples. Also, Toyama’s result entails confluence of weakly orthogonal TRSs, thus providing a syntactic criterion for proving confluence without requiring termination . We similarly introduce weakly V-orthogonal GTRSs, which are confluent. Weak V-orthogonality checking is implemented in the confluence tool , to improve its ability to deal with context-sensitive and conditional term rewriting systems.

The appropriate selection of the arguments of functions that can be evaluated in function calls is often useful to improve efficiency, speed, termination behavior, and so on. This is essential, e.g., in the conditional if - then - else operator. We can specify this by associating a set μ(f) of indices of evaluable arguments to each function symbol f . With μ (if - then - else)={1}, only the Boolean argument b in calls if b , then e else e' is evaluated. In the realm of term rewriting, this is called context-sensitive rewriting . It has been proven useful to improve the termination behavior of rewriting computations while it is still able to compute (or approximate) canonical forms like head-normal forms, (infinite) values, and (infinite) normal forms by requiring a few reasonable conditions. This article provides an overview of basic results to use context-sensitive rewriting in practice.

We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems. We follow a unified, logic-based approach to describe rewriting computations. The automatic generation of logical models for suitable first-order theories and formulas provides a common basis to implement the proofs.