Consequence Relations in Logics of AI


EPSRC Research Project EP/F014570/1
Principal Investigator:
Dr Renate Schmidt
Honorary Co-Investigator:
Dr Dmitry Tishkovsky
Start Date:
01/10/2007
End Date:
30/09/2010
Collaborating Project:
EPSRC EP/F014406/1, Manchester Metropolitan University

Summary

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.

Bibliography

1
S. Babenyshev, V. Rybakov, R. A. Schmidt, and D. Tishkovsky.
A tableau method for checking rule admissibility in S4.
Electronic Notes in Theoretical Computer Science, 262:17-32, 2010.
Preliminary version published in the Proceedings of ADDCT 2009 and Computer Science Research Report 128, Roskilde University, Denmark.

2
U. Hustadt and R. A. Schmidt.
A comparison of solvers for propositional dynamic logic.
In B. Konev, R. Schmidt, and S. Schulz, editors, Proceedings of the Second International Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh, UK, July 14, 2010, pages 60-69. EasyChair Proceedings, 2010.

3
B. Konev, R. A. Schmidt, and S. Schulz.
Proceedings of the Second International Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh, UK, July 14, 2010.
2010.

4
B. Konev, R. A. Schmidt, and S. Schulz.
Special issue on Practical Aspects of Automated Reasoning.
AI Communications, 23(2-3):67-68, 2010.

5
H. Reker.
Clausal Tableau Decision Procedures.
PhD thesis, The University of Manchester, UK.
In preparation.

6
H. Reker, R. A. Schmidt, and D. Tishkovsky.
Clausal tableau decision procedures for the two-variable fragment with equality.
In preparation.

7
R. A. Schmidt.
Automated synthesis of tableau calculi.
In T. Ball, J. Giesl, R. Hähnle, and T. Nipkow, editors, Interaction versus Automation: The two Faces of Deduction, number 09411 in Dagstuhl Seminar Proceedings, pages 13-14, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

8
R. A. Schmidt.
Simulation and synthesis of deduction calculi.
Electronic Notes in Theoretical Computer Science, 262:221-229, 2010.
Preliminary version published in Computer Science Research Report 128, Roskilde University, Denmark.


Last modified: 11 Dec 10
Copyright © 2010 Renate A. Schmidt, School of Computer Science, Univ. Man., schmidt@cs.man.ac.uk