The Temporal Semantics of Logic Programming
Naoki Yonezaki · Institutional Repositories DataBase (IRDB) · 1984
Temporal semantics of Horn logic programming and how it can be applied to reasning about a logic program are presented.In the computational model, the concept of 'world' or 'state' correspond $s$ to computational states of a program i.e. a set of substitutions and execution points.Temporal logic used in this paper is precisely defined and fundamental semantics for execution is given by a set of schemas of the logic.A general proof procedure for total correctness is also presented.Finally several extension to.Horn logic programming are considered in our framework.$g1$ .Introduction Programming languages, represented by Prolog, based on $f\cdot irst$ order predicate logic provides simple declarative semantics.First order logical deduction is used for verifying, synthesizing and translating programs, since the model theortic semantics of Horn sentences of first order predicate logic is straightforward.$[1]\sim[3]$ On the other hand, the theory of logic programming and their computations could be formalized in terms of the theory of resolution proof procedure.There exists various problems about executions of 数理解析研究所講究録 第 511 巻 1984 年 242-258