Computational Logic at RMIT

There are a number of areas of computational logic, automated reasoning, logic programming and related topics of interest to researchers in the School of Computer Science and Information Technology at RMIT University. Some of these are described below. If you are interested in any of these topics, or have any queries about anything on this page, please contact James Harland.

Research Areas

Agent Reasoning Systems

An intelligent agent system, such as a robot, or a system for air traffic control, has to make many decisions about what action to take next. There are various aspects of such reasoning, such as the available resources, the agent's predictions about the near future, the agent's goals, the dynamics of the environment and the actions of other agents. We are interested in many aspects of this kind of reasoning, including the Belief-Desire-Intention model of Rao and Georgeff (and in particular for finding appropriate inference systems for such logics), logics of expectation and observation, goal deliberation methods (particularly those based around maintenance goals), and dealing appropriately with conflicts over resources.

Flexible Protocols

Interactions between heterogeneous agents generally require methods which are much more flexible than some standard network protocols. In particular, such protocols have to be able to cope with a much more varied pattern of message passing between the agents involved. We are interested in using logical methods to assist with this problem, such as the specification of protocols, reasoning about the interactions involved, verifying that particular properties hold or reasoning about the negotiation process between agents. 

Proof Systems

Methods of inference continue to evolve, and one particular area of interest to us is that of hypersequents, which introduce a disjunctive element into proof trees.  We are particularly interested in using this technique for developing inference systems for weak intermediate logics. Other topics of interest include the detection of redundant parts of a proof tree, loop detection in proof search, re-arrangements of proofs, and the development of tableau-based methods for epistemic logics.

Logic Programming Languages

We have an abiding interest in the development of logic programming languages such as Lygon, which is based on linear logic. Of particular interest are potential logic programming languages based on extensions to linear logic, including temporal linear logic, and spatial logics. The combination of resources, time and space seems to be quite an attractive set of features for reasoning about agent interactions, messages and the like.

Busy Beaver machines

The remarkable class of Turing machines known as busy beaver machines is also of interest to members of the group.

Staff

Staff working on topics in this area include

James Harland
Michael Winikoff
Lin Padgham
John Thangarajah

Others involved in aspects of this work include

Wei Liu (University of Western Australia)
David Pym (University of Bath)

Current Students

Past Students