Semantic Properties of Computations Defined by Elementary Inference Systems
Salvador Lucas (Universitat Politecnica de Valencia)
我们考虑由 *Elementary Inference Systems* I 定义的 set/relations/computations,这些集合/relations/computations 是从 Smullyan 的 *Elementary formal systems* 获得的,使用 Gentzen 的推理规则符号,以及原子 P(t_1, ...,t_n) 的证明树,其中谓词 P 表示被考虑的 set/relation/computation。 一阶理论Th(I),实际上是一组确定的Horn子句,是给I的。 I定义的对象的属性表示为一阶句子F,在Th(I)的*canonical*模型M中,F的*satisfaction*M |=F被证明是真或假的。 因此,我们称F为I的语义属性*。 由于规范模型通常是不可计算的,因此,我们展示了如何在Th(I)的*任意*模型中通过可理解性来证明语义属性。 我们将这些想法应用于编程语言和系统的属性分析,其计算可以通过基本推理系统来描述。 特别是基于重写的系统。
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...