Semantic Properties of Computations Defined by Elementary Inference Systems

TL;DR

This paper explores the semantic properties of computations defined by elementary inference systems, linking logical inference, proof trees, and model satisfaction to analyze programming language behaviors.

Contribution

It introduces a framework connecting elementary inference systems with first-order theories and satisfaction, enabling analysis of semantic properties in programming systems.

Findings

Semantic properties can be characterized by satisfaction in models.

Canonical models are generally incomputable, but properties can be proved in arbitrary models.

Applicable to analyzing rewriting systems and programming language semantics.

Abstract

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.