In this paper we present an alternative approach to formalize the theory of logic programming. In this formalization we allow existential quantified variables and equations in queries. In opposite to standard approaches the role of answer will be played by existentially quantified systems of equations. This allows us to avoid problems when we deal with substitutions. In particular, we need no ''global'' variable separated conditions when new variables are introduced by input clauses. Moreover, this formalization can be regarded as a basis for the theory of concurrent logic languages, since it also includes a wide spectrum of parallel computational methods. Moreover, the parallel composition of answers can be defined directly -- as a consistent conjunction of answers.
翻译:在本文中,我们提出了一个将逻辑编程理论正规化的替代方法。在这种正规化中,我们允许在查询中使用存在量化变量和方程式。与标准方法相反,答案的作用将由存在量化的方程式系统来发挥。这使我们能够在处理替代问题时避免问题。特别是,当输入条款引入新的变量时,我们不需要“全球”变量。此外,这种正规化可以被视为并行逻辑语言理论的基础,因为它还包括一系列广泛的平行计算方法。此外,答案的平行构成可以被直接定义为一个一致的答案组合。