# 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.

## People |
## ORCID iD |

Ekaterina Komendantskaya (Principal Investigator) |

### Publications

Ekaterina Komendantskaya
(2011)

*Coalgebraic Proofs in Logic Programming*in Proceedings of Automated Reasoning Workshop 2011
Ekaterina Komendantskaya (Author)
(2010)

*Using Inductive Types for Ensuring Correctness of Neuro-Symbolic Computations*
Ekaterina Komendantskaya (Author)
(2011)

*SHERLOCK - an interface for Neuro-Symbolic systems*
Ekaterina Komendantskaya (Author)
(2012)

*A Statistical Relational Learning Challenge - extracting proof strategies from exemplar proofs.*
Ekaterina Komendantskaya (Author)
(2010)

*Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers*
Komendantskaya E
(2011)

*Algebraic Methodology and Software Technology*
Komendantskaya E
(2010)

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

*Artificial Neural Networks - ICANN 2010*
Komendantskaya E
(2014)

*Latest Advances in Inductive Logic Programming*
Komendantskaya E
(2011)

*Algebra and Coalgebra in Computer Science*### 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 |