Knowledge and reasoning about knowledge are fundamental notions of AI and computation. Knowledge is data and consists primarily of facts. Reasoning about knowledge involves logical inference, i.e., the ability to infer new knowledge from known facts. For the formalisation of the notions of intelligence and argumentation in all forms, logical inference is of fundamental importance. Logical inference is critically relevant in several areas of computing, ranging from AI and software engineering to computer languages and multi-agent systems.
In this joint project between the School of Computer Science at the University of Manchester and the Department of Computing and Mathematics at the Manchester Metropolitan University the aim was, finding and developing of techniques for the description of logical consequence in logics of AI and CS, with the focus being on logical consequence in modal-type logics, including traditional modal logics, temporal logics, and description logics.
The work of the team at the University of Manchester focussed on (i) developing practical methods for testing the admissibility and derivability of inference rules, and (ii) developing tableau-based decision procedures.
A significant outcome of the project is the introduction of the first tableau-based algorithm for checking the admissibility and derivability of global inference rules in modal logic. The algorithm is based on the reduction of rule admissibility to the satisfiability of a formula in a new logic extending the modal logic S4. Exploiting a tableau synthesis framework developed in a parallel EPSRC project EP/D056152/1, we were able to generate the tableau calculus from the semantic specification of this new logic. This provides the foundation for the new algorithm for determining the admissibility and derivability of inference rules.
The other main contribution of the project are clausal tableau decision procedures for the two-variable fragment of first-order logic. This closes a major gap in the area. So far it has only be known how to decide the Bernays-Schoenfinkel class, the guarded fragment and certain modal and description logics with a kind tree model property with tableau methods.
Calculi for propositional dynamic logic have been investigated since the introduction of this logic in the late seventies. Only in recent years have practical decision procedures been suggested and implemented. We have conducted a comparison of three such procedures, namely Tableau Workbench by Abate, Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009), and the MLSolver system by Friedmann and Lange (2009). The results show that caching is a promising technique in the setting of propositional dynamic logic but further optimisation to improve scalability are needed.