Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Semantic Properties of Computations Defined by Elementary Inference Systems

Salvador Lucas

TL;DR

This work introduces Elementary Inference Systems (EISs), a Gentzen-style extension of Smullyan's formal systems, to define sets, relations, and computations via proof trees. It develops a Horn-theoretic framework Th(I) for translating provability into first-order logic, and constructs canonical models (Herbrand and non-ground V-Herbrand) to study semantic properties of computations. The authors show how to prove or refute semantic properties through satisfiability in canonical or arbitrary interpretations, and demonstrate practical analysis on Generalized Term Rewriting Systems using tools like AGES, Mace4, and Prover9. The approach enables precise, model-theoretic reasoning about programming languages and rewriting-based systems, bridging operational semantics with first-order logic and providing a scalable method for semantic analysis. The work also clarifies how to ground non-ground interpretations and how to leverage inductive and logical-consequence reasoning to capture a range of semantic properties in a uniform framework.

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.

Semantic Properties of Computations Defined by Elementary Inference Systems

TL;DR

This work introduces Elementary Inference Systems (EISs), a Gentzen-style extension of Smullyan's formal systems, to define sets, relations, and computations via proof trees. It develops a Horn-theoretic framework Th(I) for translating provability into first-order logic, and constructs canonical models (Herbrand and non-ground V-Herbrand) to study semantic properties of computations. The authors show how to prove or refute semantic properties through satisfiability in canonical or arbitrary interpretations, and demonstrate practical analysis on Generalized Term Rewriting Systems using tools like AGES, Mace4, and Prover9. The approach enables precise, model-theoretic reasoning about programming languages and rewriting-based systems, bridging operational semantics with first-order logic and providing a scalable method for semantic analysis. The work also clarifies how to ground non-ground interpretations and how to leverage inductive and logical-consequence reasoning to capture a range of semantic properties in a uniform framework.

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.

Paper Structure

This paper contains 19 sections, 14 theorems, 25 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. First-order logic
  4. Generalized Term Rewriting Systems
  5. Elementary Inference Systems
  6. Proofs with Elementary Inference Systems
  7. First-Order Theory of an Elementary Inference System
  8. Models of Elementary Inference Systems
  9. Herbrand interpretations.
  10. Least Herbrand model of an EIS
  11. Least V-Herbrand model of an EIS
  12. Grounding the least V-Herbrand model
  13. Semantic Properties of Elementary Inference Systems
  14. Semantic Properties as Logical Consequences
  15. Semantic Properties as Inductive Consequences
  16. ...and 4 more sections

Key Result

Proposition 9

Let $\mathcal{}\hbox{$\mathcal{I}$}$ be an EIS, $A$ be an atom, and $\sigma$ be a substitution. If ${\vdash_{\mathcal{}\hbox{$\mathcal{I}$}}A}$, then ${\vdash_{\mathcal{}\hbox{$\mathcal{I}$}}\sigma(A)}$.

Figures (3)

  • Figure 1: Elementary inference system $\mathcal{}\hbox{$\mathcal{I}$}(\mathcal{}\hbox{$\mathcal{R}$})$ for $\mathcal{}\hbox{$\mathcal{R}$}$ in Example \ref{['ExPEvenZeroOdd']}
  • Figure 2: Generic elementary inference rules for a GTRS
  • Figure 3: Theory ${\overline{\mathcal{}\hbox{$\mathcal{R}$}}}$ for $\mathcal{}\hbox{$\mathcal{R}$}$ in Example \ref{['ExPEvenZeroOdd']}

Theorems & Definitions (41)

  • Example 1
  • Example 2
  • Example 3
  • Definition 4: Elementary inference system
  • Remark 5
  • Definition 6: EIS of a GTRS
  • Definition 7: Provable atom
  • Remark 8
  • Proposition 9
  • Definition 10
  • ...and 31 more