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

Computational Logic in Artificial Neural Networks

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

基本信息

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

来源：
https://gtr.ukri.org/projects?ref=EP%2FF044046%2F1
关键词：
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]中，哥德尔证明了，在每一个足够强的形式系统中，存在一个不可判定的命题。由此可见，希尔伯特的纲领不可能实现，正如丘奇和图灵所证明的那样。然而，即使在这些结果之后，人们仍然对如何创造某种自动推理的主要问题感兴趣，或者，正如后来所说的那样，人工智能。这是一个悬而未决的问题，人类思维是否按照某种预定义的算法行事，这种算法是否合理，它是否可以被人类合理地形式化，以及如果形式化，它是否可以被证明是合理的。图灵的机器刺激了数字计算机的诞生;生物学和神经科学成为了真正的科学学科。所有这些进步都增加了人们对创造一种人工智能形式的普遍问题的兴趣。联结主义是人工智能、认知科学、神经科学、心理学和心灵哲学领域的一场运动，它希望用人工神经网络的想法/人脑的简化数学模型来解释人类的智力能力。神经符号整合（Neuro-Symbolic Integration）是神经网络的一个研究领域，它研究如何将逻辑和形式语言与神经网络相结合，以更好地理解符号（演绎）和人类（发展、自发）推理的本质，并展示它们之间的相互联系。然而，它们很少用于自动推理和计算逻辑。现在是开发现有神经符号网络替代方案的正确时机;为此，我们提出的SLD神经网络似乎是最合适的候选者。SLD神经网络使用一种新的方法来执行经典逻辑程序的一阶SLD分解算法。由此产生的神经网络是有限的，并体现在neurocounting.We认可的六个学习功能，我们建议测试我们的SLD神经网络，并将其应用到更广泛的一类逻辑程序和逻辑。这将引导我们评估它们的有效性，一方面将它们与自动推理中使用的正统方法进行比较，另一方面将它们与计算逻辑中使用的替代（非神经）网络进行比较。该项目的高潮将是创建一个更通用，更抽象的神经网络解释器，可用作广泛的逻辑和逻辑程序的自动证明器。通过实现其目标，该项目将对刺激神经符号整合和认知科学领域的研究产生长期影响。