The Formalized Procedural Semantic Of Logic Programming Language G(?)del

G(o|¨)del is a declarative logic programming language succeeded to Prolog.It is based on many-sorted first order logic with parametric polymorphism,discards the features of Prolog which are non-logical,introduces type system,integrates the merit of many languages,adds some new language components which let it be efficient declarative programming language.However,the complexity of G(o|¨)del is greatly increased with the introduction of type system,modular structure,delay calculation, pruning operation.Because the methods and techniques in compiler of the logic programming language with recursive and descriptive characteristics are completely different from that used in the compiler of process-oriented programming language, the methods and techniques of the latter can not transplantation.Since the basic theory research lags behind,so the research and development of the compiler system of G(o|¨)del is still in slow progress.In order to facilitate the spread and in-depth research of G(o|¨)del,our project group brought forward a set of theoretical foundation based on Horn subset of typed first-order logic.This paper emphasized strict formalized procedural semantic of G(o|¨)del based on grammar and formalized declarative semantic of the language which can lay a reliable theoretical basis for the realization of the compiler system of G(o|¨)del.This paper introduced grammar of G(o|¨)del in the first part,and described formalized procedural semantic based on typed first-order logic detailedly in the second part,which discussed ground type,constructive type and structral type, brought in type compatibility,type deductive algorithm and type constraint algorithm, unification algorithm based on the theory and SLD resolution refutation.Then,in the following part,each module of G(o|¨)del programming design were introduced.Finally, on the basis of original G(o|¨)del system model,we perfected the design methodology of the system based on type system.Under the support and direction of relative theories, with more following tasks being carried out and the progressively maturation of the G(o|¨)del compiler system realizing technology,G(o|¨)del language will catch more attention.