Semantic Properties of Computations Defined by Elementary Inference Systems
Salvador Lucas · Electronic Proceedings in Theoretical Computer Science · 2025
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.