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.