Godel语言是继Prolog语言之后出现的逻辑程序设计语言，它建立在多态多类的一阶逻辑基础之上，摒弃了Prolog语言中的非逻辑成分，集成了许多语言的有效成分和优点，引入了类型系统，这使得它成为一种高效的说明性逻辑程序设计语言。然而，时至今日，Godel语言编译系统的开发研究仍然进展缓慢，主要原因是多态多类的类型系统、模块化结构、延迟计算、剪枝操作等多种新语言成分和机制的引入，使逻辑程序设计语言Godel的复杂程度大大提高，而面向过程程序设计语言的编译方法和技术完全不同于具有递归性、说明性特点的逻辑程序设计语言，先前关于Prolog语言的编译方法和技术不能简单移植和照搬，而理论基础研究的滞后直接导致系统研究和开发进展缓慢，迄今尚无新的进展和系统开发成果报道。 为了促进Godel语言的推广以及深入研究，本文着眼于编译系统的设计与实现，为Godel语言建立了严格的数学基础，包括其语法和说明性语义理论，从而为其深入研究和编译实现奠定了可靠的部分理论基础。 鉴于传统的一阶逻辑语言的局限性，本文首先对传统的一阶语言进行扩展，引入类型，提出了类型一阶语言，完整地给出了类型一阶语言的语法定义.初步建立了带类型的一阶逻辑理论。论文针对类型一阶语言中的Horn子集给出了Godel语言(子集)的语法部分。在此基础上，给出了解释或赋值的一般定义，然后讨论在合理的解释下类型合式公式的真假值判别法，并由此建立起带类型的一阶逻辑系统的模型。接着，利用类型一阶语言的H-模型探讨了Godel程序的形式化说明性语义，最终得出结论为最小H-模型MP可以作为程序P的形式语义，其理由是MP恰由作为P的逻辑推论的那些基原子组成。 本文最后还给出了Godel语言控制机制的一种实现算法，可以为该语言的完全实现提供重要支持。