The Post
The successful candidate will undertake a three year project to
investigate and develop "Proof Methods for
Multi-Agent Systems",
carrying out, publicising and disseminating high quality research.
Project environment
The work will take place within the Formal Methods
Research Group in the Department of Computer Science
at the University of
Manchester, under the supervision of Dr
Renate Schmidt, who is an expert on automated proof methods,
resolution decision procedures, solvable first-order fragments,
non-classical logics and relation algebras. Co-investigators in this
project are
Prof. Michael
Fisher, who has an international reputation in logic, agent-based
systems and programming languages, and
Dr Clare Dixon, who has an
international reputation in temporal reasoning, automated
theorem-proving, and verification; both are from the
Centre for Agent
Research and Development at the Manchester Metropolitan University.
Person specification
-
A Ph.D. in Computer Science or Mathematics or equivalent experience.
-
Knowledge of modal logic, temporal logic, first-order logic, proof
theory, automated reasoning.
-
Ability to work collaboratively.
-
Good communication skills, both oral and written.
Background
Agent-Based Systems is widely recognised as an area of rapidly
increasing importance [14,
13]. Agents provide a key abstraction within modern
development of AI systems and software. Although there exist powerful
theoretical models of agency [10,
11, the techniques for solving the reasoning
problem within these theories have not been investigated sufficiently
and proof systems have not been applied in practical agent systems.
This project aims to apply the know-how and tools established and
produced in previous work to develop proof methods for the expressive
combinations of diverse logics used in agent theories, and apply these
to particular examples from agent-based systems.
A multi-agent system is a collection of semi-autonomous processes known
as `agents' which live in dynamic and unpredictable environments.
Agents continuously interact which each other and the environment and
need to reason about their own and other agent's attitudes. A number of
theoretical frameworks specifying agent-based systems have been
proposed, for example, the BDI model being developed at AAII in
Australia [17], 18], the powerful KARO framework being developed at Utrecht
University [20], temporal logics
of knowledge and belief [4,
5, 6], and also more
recent developments in modal description logics
[1, 21].
These theories are
being used for the specification and formalisation of agent-based
systems, yet the much needed techniques to analyse and manipulate such
specifications, utilising symbolic information to determine appropriate
behaviour, are only slowly beginning to emerge
[15]. For example, tableaux
for multi-modal belief or knowledge logics
[5], tableaux for multi-modal
belief or knowledge logics with linear-time temporal logic
[23], tableaux for
belief-desire-intention logics with either linear or branching-time
temporal logics [17], and resolution for knowledge logics with linear-time
temporal logics [2].
The key problem in addressing the reasoning problem within multi-agent
systems is the inherent complexity of the agent scenarios. The logics
introduced in existing specification frameworks usually incorporate
combinations of multi-modal logics, temporal logics and first-order
logic. The degree to which combinations of these are useful and
manageable depends on the kind of interactions existing between the
logics. These vary in kind and complexity in different systems.
Although the basic properties of some of the individual logics are
well-understood, less is known about different interactions, and very
little work has been carried out on proof methods for such complex
logics.
Aims and objectives
The long term goal of this work is to provide practical proof systems and
automated reasoning tools for the development of multi-agent systems.
Work in this project will focus on the reasoning problem for complex
combinations of expressive modal logics, temporal logics and first-order
logic as well as unconventional application-oriented logics which form
the basis of common specification frameworks for modelling agent
behaviour. Powerful proof techniques are now available and provide
viable means for efficient and practical reasoning in a wide range of
non-classical logics and first-order classes
[3,
7,
8, 9,
10, 11,
12,
13,
16,
19].
The intention is to study to what extent these new methods can be
utilised and enhanced for the development of feasible proof systems
suitable to meet the reasoning needs of agent-based systems.
The principal objectives for this project are:
-
The investigation of the computational properties of
interactions common in multi-agent systems.
-
The development, where possible, of terminating, automatic proof
procedures.
-
The identification of general principles correlating particular
logics, clausal classes or their combinations, with particular techniques
for guiding search during the computation.
-
The investigation to which extent sound and complete proof procedures
of single logics can be combined to form sound and complete proof
procedures for the combination of these logics.
References
-
Baader, F. and Ohlbach, H. J. (1995),
A Multi-Dimensional Terminological Knowledge Representation Language.
J. Appl. Non-Classical Logics
2
153-197.
-
Dixon, C. and Fisher, M. and Wooldridge, M. (1998),
Resolution for Temporal Logics of Knowledge.
J. Logic Computat.
8 (3) 345-372.
-
Ganzinger, H. and Hustadt, U. and Meyer, C. and Schmidt, R. A. (1999),
A Resolution-Based Decision Procedure for Extensions of K4.
To appear in Advances in Modal Logic, Vol. 2, CSLI
Publ.,
-
Fagin, R. and Halpern, J. Y. and Moses, Y. and Vardi, M. Y. (1995),
Reasoning About Knowledge.
MIT Press.
-
Halpern, J. Y. and Moses, Y. (1992),
A Guide to Completeness and Complexity for Modal Logics of Knowledge and
Belief.
Artif. Intell.
54
319-379.
-
Halpern, J. Y. and Vardi, M. Y. (1989),
The Complexity of Reasoning about Knowledge and Time. I Lower Bounds.
J. Computer and System Sci.
38
195-237.
-
Hustadt, U., Dixon, C., Schmidt, R. A. and Fisher, M. (2000),
Normal Forms
and Proofs in Combined Modal and Temporal Logics.
Proc. FroCoS'2000.
LNAI,
Springer,
To appear.
-
Hustadt, U. and Schmidt, R. A. (1997),
On Evaluating Decision Procedures for Modal Logics.
Proc. IJCAI'97.
1
Morgan Kaufmann,
202-207.
-
Hustadt, U. and Schmidt, R. A. (1998),
Simplification and Backjumping in Modal Tableau.
Proc. TABLEAUX'98.
LNCS 1397 Springer, 187-201.
-
Hustadt, U. and Schmidt, R. A. (1999),
An Empirical Analysis of Modal Theorem Provers.
J.\ Appl.\ Non-Classical Logics
9
(4)
479-522.
-
Hustadt, U. and Schmidt, R. A. (1999),
On the Relation
of Resolution and Tableaux Proof Systems for Description Logics.
In
Proc. IJCAI'99.
Morgan Kaufmann,
110-115.
-
Hustadt, U. and Schmidt, R. A. (1999),
Maslov's Class K Revisited.
In
Automated Deduction-CADE-16.
LNAI 1632,
Springer,
172-186.
-
Hustadt, U. and Schmidt, R. A. (2000),
Issues of
Decidability for Description Logics in the Framework of Resolution.
In
Automated Deduction in Classical and Non-Classical Logics.
LNAI 1761,
Springer,
192-206.
-
Jennings, N. R. and Wooldridge, M. (1998),
Applications of Agent Technology.
In Agent Technology: Foundations, Applications, and Markets.
Springer.
-
Ndumu, D. T. and Nwana, H. S. (1997),
Research and Development Challenges for Agent-Based Systems.
IEE Proc. Softw. Eng.
144 (1).
-
Ohlbach, H. J. and Schmidt, R. A. (1997),
Functional Translation
and Second-Order Frame Properties of Modal Logics.
J. Logic Computat.
7
(5)
581-603.
-
Rao, A. S. (1996),
Decision Procedures for Propositional Linear-Time
Belief-Desire-Intention Logic.
In Proc. ATAL'95.
LNAI 1037, Springer, 102-118.
-
Rao, A. S. and Georgeff, M. P. (1991),
Modeling Rational Agents within a BDI-Architecture.
In
Proc. KR'91.
Morgan Kaufmann,
473-484,
-
Schmidt, R. A. (1999),
Decidability by
Resolution for Propositional Modal Logics.
J. Automated Reasoning
22
(4)
379-396.
-
Van Linder, B. and van der Hoek, W. and Meyer, J.-J. C. (1998),
Formalizing Abilities and Opportunities of Agents.
Fundameta Informaticae
34 (1, 2) 53-101.
-
Wolter, F. and Zakharyaschev, M. (1998),
Satisfiability Problem in Decsription Logics with Modal Operators.
In Proc. KR-98.
Morgan Kaufmann,
512-513.
-
Wooldridge, M. (1998),
Agent-Based Computing.
Interoperable Comm. Networks
1 (1) 71-97.
-
Wooldridge, M. and Dixon, C. and Fisher, M. (1998),
A Tableau-Based Proof Method for Temporal Logics of Knowledge and
Belief.
J. Appl. Non-Classical Logics
8
(3)
225-258.
Advert |
Further details |
General Information for applicants
Renate A. Schmidt
Home |
Publications |
Tools |
FM Group |
Dept Computer Science |
Man Univ
Last modified: 11 Feb 2000
Copyright © 2000
Renate A. Schmidt,
Dept Computer Science, Man Univ, schmidt@cs.man.ac.uk