权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Computational Logic in Artificial Neural Networks

人工神经网络中的计算逻辑

基本信息

批准号：
EP/F044046/2
负责人：
Ekaterina Komendantskaya
金额：
--
依托单位：
University of Dundee
依托单位国家：
英国
项目类别：
Fellowship
财政年份：
2010
资助国家：
英国
起止时间：
2010 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FF044046%2F2
关键词：
Computational Logic Artificial Neural Networks

项目摘要

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.

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