Computational Logic in Artificial Neural Networks

Lead Research Organisation: University of Dundee
Department Name: School of Computing

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
Ekaterina Komendantskaya (2011) Coalgebraic Proofs in Logic Programming in Proceedings of Automated Reasoning Workshop 2011

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

publication icon
Komendantskaya E (2010) Artificial Neural Networks - ICANN 2010

publication icon
Komendantskaya E (2010) Unification neural networks: unification by error-correction learning in Logic Journal of IGPL

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 During this grant, I was working on inter-disciplinary methods for building Artificial Intelligence applications involving formal logic reasoning and machine learning. This involved both building a suitable theory and implementing an application.

The results were published in conference proceedings and journals; and informed further, improved applications developed in the next grant EP/J014222/1.

During this project, I have also started a new but related research direction: studying infinite (also called coalgebraic) computations in logic programming. The work done in 2008-2011 laid foundations for several publications on the topic, and another grant EP/K031864/1.
Exploitation Route The findings led to several collaborative papers, projects and workshops in Academia. The papers produced in 2008-11 during this grant gathered in total 118 citations, according to Google Scholar (Oct 2014).

Also, they partially made their way to industry via later SICSA Industrial Grant (2012-2014).
Sectors Digital/Communication/Information Technologies (including Software)

URL http://staff.computing.dundee.ac.uk/katya/CLANN/index.html
 
Description Coalgebraic Logic Programming for Type Inference: parallelism and corecursion for a new generation of programming languages
Amount £280,590 (GBP)
Funding ID EP/K031864/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 09/2013 
End 01/2017
 
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 Industrial Proof of Concept grant Machine-Learning for Industrial Theorem Proving
Amount £10,000 (GBP)
Organisation SICSA Scottish Informatics and Computer Science Alliance 
Sector Academic/University
Country United Kingdom
Start 09/2013 
End 04/2014
 
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
 
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