Semantic Properties of Computations Defined by Elementary Inference Systems

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.