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) go one step further and employ, 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.
In all cases studied so far, the logic of the CLDS is strictly more powerful than the logic it aims to simulate, and some restrictions on initial conditions must be made. Much of this work is in collaboration with Dr. Alessandra Russo. A slightly different approach, applied to logic and probability, can be found in Bjorn Bjurling's PhD Thesis
Further steps in this programme are to investigate the use of the full power of the CLDS, without restrictions, and to use the approach to derive new logics, most likely by combining two or more logics from the same or from different families. In this latter application, just as the set of inference rules used in a CLDS have a uniform format, with variations for different logics, so a set of bridging rules need to be formulated, again with possible variations for differing circumstances.
This work is in collaboration with Dr. Alessandra Russo and our joint PhD student Jiefei Ma.
Together with Dr. Alessandra Russo I co-supervised Dr Oliver Ray for his PhD and work on HAIL. I am now co-supervising Tim Kimber on Induction on Failure, extending ILP to learn multi-clause theories.
This activity is carried out mostly through student projects at present.
This work, together with Dr Chris Hogger, concerns how to synthesise minimal reactive programs, which are similar to production rules but have the addition of an implicit goal. Our approach introduces a "situation graph" and evaluates policies over this graph using Bellman's discounted reward equation and is applicable to multi-agent environments. We have devised several algorithms for finding optimal policies (with respect to reward obtained) and investigated consequences of abstractions of the situation graph.
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. Previous work in collaboration with Dr Artur Garcez investigated the extraction of learned knowledge from propositional networks as rules. I am now interested in learning and extraction of rules in relational networks. See the distinguished MSc dissertation of Mathieu Guillaume-Bert (PG 2009) for an exciting approach to this topic. .