基本推理系统所定义计算之语义性质 (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.

翻译：本文研究由*基本推理系统* I 所定义的集合/关系/计算，该系统采用根岑的推理规则记法改进斯穆里安的*基本形式系统*，并通过证明树处理原子公式 P(t_1,...,t_n)，其中谓词 P 表征所考察的集合/关系/计算。系统 I 被赋予一个一阶理论 Th(I)——实质上为一组确定性子句。由 I 定义的对象性质通过一阶语句 F 表达，其真伪通过 Th(I) 的*典范*模型 M 中 F 的*满足关系* M |= F 进行判定。鉴于此，我们称 F 为 I 的*语义性质*。鉴于典范模型通常不可计算，本文展示了如何通过 Th(I) 的*任意*模型 A 中的可满足性来（反）证明语义性质。我们将这些思想应用于分析可通过基本推理系统描述计算的编程语言与系统之性质，特别是基于重写的系统。