Computational Logic in Artificial Neural Networks

Lead Research Organisation: University of St Andrews
Department Name: Computer Science

Abstract

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.

Publications

10 25 50

publication icon
Bertot Y (2008) Inductive and Coinductive Components of Corecursive Functions in Coq in Electronic Notes in Theoretical Computer Science

publication icon
Ekaterina Komendantskaya (2009) Parallel Term Rewriting in Artificial Neural Networks in ICNC'09 electronic Proceedings

publication icon
Ekaterina Komendantskaya (2009) Neurons or Symbols: why does Or remain exclusive? in ICNC'09 Proceedings

publication icon
Ekaterina Komendantskaya (Author) (2009) Intermediate three -valued regular logics of Kleene in Logic Studies

publication icon
Ekaterina Komendantskaya (Author) (2011) SHERLOCK - an interface for Neuro-Symbolic systems

publication icon
Ekaterina Komendantskaya (Author) (2009) Parallel Rewriting in Neural Networks

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/F044046/1 01/10/2008 31/03/2010 £241,846
EP/F044046/2 Transfer EP/F044046/1 01/04/2010 30/09/2011 £124,269
 
Description The fundamental problem of creating (and then evaluating) automated reasoning system based upon some formally defined logical calculus has been tackled for centuries.

One can argue that the problem is as old as mathematical logic and even computational mathematics. Among famous pioneers in this field were Boole, Peano, 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 some logical calculus. This program is now commonly called ``Hilbert's Programme".



In the famous Incompleteness Theorem [1931] Godel proved that there are undecidable propositions in every axiomatic theory, and thus showed that Hilbert's program cannot be

accomplished. Equivalent theorems were proven by Turing and Church.



However, even after the famous result of Godel, Turing and Church, the major question of how one can create some kind of automated reasoning, or, as it was later called, artificial intelligence, remained appealing. It remains an open question whether 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 proved to be sound.



Turing's machines stimulated the creation of digital computers; biology and neuroscience became proper scientific disciplines. And all this progress only increased interest in the general problem of creating an 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 artificial neural networks - 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.



This EPSRC grant was devoted to studies of various neuro-symbolic methods applicable in automated reasoning. The first research objective was to implement two logic algorithms -- first-order unification and first-order term rewriting -- in artificial neural networks. This goal was achieved, and the software is now published on-line on the project's webpage; the major results are published in journal and conference proceedings.



This work was taken to a more general and abstract level by a successive novel method ML-CAP (for ``machine-learning coalgebraic automated proofs") that can use statistical machine learning tools such as Support Vector Machines and Neural networks to determine general properties of formal proofs by detecting variations of proof patterns. The novel ML-CAP method was developed and formulated during the EPSRC PDRF fellowship.

Among other things, this method required a careful study of coalgebraic semantics of logic programs, which was undertaken during this grant. These studies led to a new coalgebraic proof procedure for first-order logic programs and laid foundations for the ML-CAP.

The method ML-CAP has become the subject of my present and future studies, and is already approved for support by the EPSRC First-grant scheme.



The following objectives were achieved:

1. To represent the operational semantics of logic programming languages as (artificial) neural networks.

2. To evaluate the effectiveness of these representations compared with orthodox methods such as resolution and analytic tableaux.

3. To refine these representations in the light of evaluations.

4. To seek abstract and more general representations of which the above representations are special cases.

5. To test, implement and experiment with (existing) SLD Neural Networks and the neural networks yet to be obtained (as above), using standard neural networks software.

6. To look for more broad implementation of the developed techniques in automated reasoning and proof theory.







However, the evaluation stage of the proposal showed that the proposed method was not optimal. I went on working on a deeper methods that capture statistical aspects of automated theorem proving, and in the last year of my project, I developed a new alternative method for machine-learning coalgebraic automated proofs (ML-CAP) that lay foundation for my new EPSRC grant ML-CAP. Therefore, one can say that there were two main categories of research results acheived within the EPSRC PRRF - and that is implementation and evaluation of the method I had proposed for the Fellowship, and development of a novel, more optimal and successful method that forms my long-term research agenda.
Exploitation Route The research can be adapted for use in a range of industrial-scale Artificial Intelligence Applications. The project's web-page provides a guide for anyone wishing to use the produced software or exploit the theoretical results.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://www.computing.dundee.ac.uk/staff/katya/CLANN/index.html
 
Description MACHINE LEARNING COALGEBRAIC AUTOMATED PROOFS
Amount £100,268 (GBP)
Funding ID EP/J014222/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 02/2012 
End 02/2014
 
Description SICSA Distinguished Visitor J.Power
Amount £3,060 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 07/2010 
End 08/2010
 
Description SICSA Distinguished Visitor K.U.Kuhnberger
Amount £2,200 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 10/2009 
End 11/2009
 
Description SICSA Workshop Funding STP 2011
Amount £400 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 06/2011 
End 07/2011
 
Description Neuro-Symbolic discussion group 
Organisation City, University of London
Country United Kingdom 
Sector Academic/University 
PI Contribution The partnership between the Universities of Dundee, St Andrews, Imperial College, and City University London
Start Year 2009
 
Description Neuro-Symbolic discussion group 
Organisation Imperial College London
Country United Kingdom 
Sector Academic/University 
PI Contribution The partnership between the Universities of Dundee, St Andrews, Imperial College, and City University London
Start Year 2009
 
Title CLANN software 
Description Experimental software supporting experiments on Neuro-symbolic tools for performing unification and term-rewriting in neural networks. 
Type Of Technology Software 
Year Produced 2009 
Open Source License? Yes  
Impact The impact was mainly research/academic. 
URL http://staff.computing.dundee.ac.uk/katya/CLANN/CLANNsoftware.html