Computational Logic in Artificial Neural Networks

基于正式定义的逻辑演算创建(然后评估)自动推理系统的基本问题已经被考虑了几个世纪。可以说，这个问题和数理逻辑甚至计算数学一样古老。这一领域的先驱包括布尔、皮亚诺和希尔伯特。希尔伯特在试图找到恰当的数学基础和恰当的形式演算时，宣布了使用逻辑演算将数学形式化的计划。这个项目现在通常被称为希尔伯特项目。然而，在他著名的不完全性定理[1931]中，哥德尔证明了，在每个足够强的形式系统中，都有一个不可判定的命题。正如丘奇和图灵所表明的那样，希尔伯特的计划是无法完成的。然而，即使在这些结果之后，人们仍然感兴趣的主要问题是如何创建某种自动推理，或者后来被称为人工智能的推理。人类的大脑是否按照某种预定义的算法行事，这个算法是否合理，它是否可以被人类完美地形式化，以及如果形式化，它是否可以被证明是健全的，这是一个悬而未决的问题。图灵的机器刺激了数字计算机的创造；生物学和神经科学成为适当的科学学科。所有这些进步增加了人们对创造一种形式的人工智能这一普遍问题的兴趣。连接主义是人工智能、认知科学、神经科学、心理学和心灵哲学领域的一场运动，希望用人工神经网络/人脑的简化数学模型的想法来解释人类的智力能力。它的一个领域，神经符号集成，研究如何将逻辑和形式语言与神经网络相结合，以便更好地理解符号(演绎)和人类(发展中的、自发的)推理的本质，并显示它们之间的相互联系。然而，它们很少被用于自动推理和计算逻辑。现在是开发一种替代现有神经符号网络的合适时机；为此，我们提出的SLD神经网络似乎是最合适的候选者。SLD神经网络使用一种新的方法来执行神经网络中经典逻辑程序的一阶SLD归结算法。得到的神经网络是有限的，包含神经计算中公认的六个学习函数。我们建议测试我们的SLD神经网络，并将它们应用于更广泛的逻辑程序和逻辑类别。这将导致我们评估它们的有效性，一方面将它们与自动推理中使用的正统方法进行比较，另一方面与计算逻辑中使用的替代(非神经)网络进行比较。该项目的最终结果将是创建一个更通用、更抽象的神经网络解释器，准备用作广泛类别的逻辑和逻辑程序的自动证明器。通过实现其目标，该项目将产生长期效果，促进神经符号整合和认知科学领域的研究。

The fundamental problem of creating (and then evaluating) automated reasoning systems based upon formally defined logical calculi has been considered for centuries. Arguably, the problem is as old as mathematical logic and even computational mathematics.Among the pioneers in this field were Boole, Peano and Hilbert. Hilbert, in his attempts to find proper foundations of mathematics and a proper formal calculus for it, announced the programme of formalising mathematics using a logical calculus. This program is now commonly called Hilbert's Programme . However, in his well-known Incompleteness Theorem [1931], Gdel proved that, in every sufficiently strong formal system, there is an undecidable proposition. It follows that Hilbert's programme cannot be accomplished, as shown by Church and Turing. However, even after these results, the major question, of how one can create some kind of automated reasoning, or, as it was later called, artificial intelligence, remained of interest. It is an open question whether the human mind acts in accordance with some pre-defined algorithm, whether this algorithm is sound, whether it can be soundly formalised by humans, and whether, if formalised, it can be shown to be sound. Turing's machines stimulated the creation of digital computers; biology and neuroscience became proper scientific disciplines. All this progress increased interest in the general problem of creating a form of artificial intelligence.Connectionism is a movement in the fields of artificial intelligence, cognitive science, neuroscience, psychology and philosophy of mind which hopes to explain human intellectual abilities using the idea of an artificial neural network / a simplified mathematical model of a human brain. One of its areas, Neuro-Symbolic Integration, investigates ways of integrating logic and formal languages with neural networks in order to better understand the essence of symbolic (deductive) and human (developing, spontaneous) reasoning, and to show interconnections between them.Many neuro-symbolic systems have been proposed over the last two decades. However, they have been little used in automated reasoning and computational logic. Now is the right time for development of an alternative to the existing neuro-symbolic networks; for this, our proposed SLD neural networks appear to be a most suitable candidate. SLD neural networks use a novel method of performing the algorithm of first-order SLD-resolution for classical logic programs in neural networks. The resulting neural networks are finite, and embody six learning functions as recognised in neurocomputing.We propose to test our SLD neural networks and apply them to a broader class of logic programs and logics. This will lead us to evaluate their effectiveness, comparing them with orthodox methods used in automated reasoning, on the one hand, and with alternative (non-neural) networks used in computational logic, on the other hand. The culmination of the project will be the creation of a more general, and more abstract, neural network interpreter ready to be used as an automated prover for a broad class of logics and logic programs. By achieving its objectives, the project will have a long-term effect of stimulating research in the areas of Neuro-Symbolic Integration and Cognitive Science.