Logic Programming Related Research
- This work is in collaboration with
- Distributed Abductive Reasoning (DARE):This work was with our previous PhD student Jiefei Ma.
- Inductive Logic Programming (ILP):Includes work with a previous PhD student Dr Oliver Ray on Hybrid Abductive and Inductive learning: HAIL. This was followed up by work with previous PhD student Tim Kimber on Induction on Failure, which extended ILP to learn multi-clause theories for normal logic programs. Current work with PhD student Mark Law is on learning Answer set programs (ASP) and with PhD student Duangtida Athakravi is on Abductive learning using ASP through theory revision.
- Probability in Logic Programming:Current work with PhD student Calin-Rares Turliuc is on probabilistic abductive logic programming, which has been applied to computational biology in collaboration with Professor Rob Krams and PhD student Nataly Maimari in Bioengineering.
- Application of Logic Programming to Ontologies:PhD student Graham Deane is investigating approaches using ASP to detecting inconsistencies in Ontologies.
- Implementing Novel Theorem Provers
- This activity is carried out mostly through student projects at present.
- Policies for (teleo)Reactive Agents
- This work, together with Dr Chris Hogger, was concerned with synthesis of minimal reactive programs, which are similar to production rules but have the addition of an implicit goal. Our approach introduced the notion ofsituation grap and evaluated policies over this graph using Bellman’s discounted reward equations. We devised several algorithms for finding optimal policies (with respect to reward obtained) and investigated consequences of abstractions of the situation graph and applications to multi-agent environments.
- Neural-Symbolic Integration
- Knowledge in the form of logic programs can be encoded into artificial neural networks with an input and output layer, together with a single hidden layer. By training such networks using back-propagation, additional knowledge can be encoded. This work is in collaboration with Dr Artur Garcez. We investigated the extraction of learned knowledge from propositional networks as rules. Extraction of rules in relational networks was investigated by MSc student Mathieu Guillaume-Bert. See his distinguished MSc dissertation (PG 2009) for an exciting approach to this topic.
- Current interest is in applying neural networks to learning grammars and other structured data using neural networks. This activity is carried out mostly through student projects at present.
- Labelled Deductive Systems (LDS)
- LDS provide a uniform approach for investigating different logics, both from one family and from different families, by the use of labelled formulas of the form wff:label. Different families of logics interpret the labels in different ways, whereas logics of the same family use the same interpretation but impose different properties on the labels. In this way, many different resource logics can be uniformly represented, as can many different modal logics.Work on LDS and Tableaux methods was initiated in the EPSRC supported project ADULT (GR/J/14715), 1993-1996. Algorithmic Deduction with Labelled Tableaux (Final report)Compiled LDS (CLDS) in collaboration with with Dr. Alessandra Russo. goes one step further and employs, in a uniform way, a first order semantics for LDS, so that automation is possible via adaptations of standard theorem provers. So far, the families of modal logics and resource logics,including fuzzy logic, have been fully studied and the results published. (See Krysia Broda, Dov Gabbay, Luis Lamb and Alessandra Russo. Compiled Labelled Deductive Systems: A Uniform Presentation of Non-Classical Logics, Research Studies press, 2004 ISBN 0863802966.)Other logics for which the approach is applicable include Description Logic, Hybrid Logics, Term Modal Logics and logics based on the ambient calculus. Natural deduction, tableaux methods and refutation theorem provers have been used as the proof method at the first order level, whilst natural deduction and tableaux methods have been used at the CLDS level. See the distinguished MSc dissertation of Aikaterina Marazopoulou (PG 2009) for a formal framework for CLDS using tableau systems.
A slightly different approach, applied to logic and probability, can be found in Bjorn Bjurling’s PhD Thesis
- LDS provide a uniform approach for investigating different logics, both from one family and from different families, by the use of labelled formulas of the form wff:label. Different families of logics interpret the labels in different ways, whereas logics of the same family use the same interpretation but impose different properties on the labels. In this way, many different resource logics can be uniformly represented, as can many different modal logics.Work on LDS and Tableaux methods was initiated in the EPSRC supported project ADULT (GR/J/14715), 1993-1996. Algorithmic Deduction with Labelled Tableaux (Final report)Compiled LDS (CLDS) in collaboration with with Dr. Alessandra Russo. goes one step further and employs, in a uniform way, a first order semantics for LDS, so that automation is possible via adaptations of standard theorem provers. So far, the families of modal logics and resource logics,including fuzzy logic, have been fully studied and the results published. (See Krysia Broda, Dov Gabbay, Luis Lamb and Alessandra Russo. Compiled Labelled Deductive Systems: A Uniform Presentation of Non-Classical Logics, Research Studies press, 2004 ISBN 0863802966.)Other logics for which the approach is applicable include Description Logic, Hybrid Logics, Term Modal Logics and logics based on the ambient calculus. Natural deduction, tableaux methods and refutation theorem provers have been used as the proof method at the first order level, whilst natural deduction and tableaux methods have been used at the CLDS level. See the distinguished MSc dissertation of Aikaterina Marazopoulou (PG 2009) for a formal framework for CLDS using tableau systems.