Logic and Computation Group

Research

The link between logic and computation is well established, and dates back at least as far as the early days of modern computer science, with the works of Turing, Gödel and others being obvious examples.

Logic provides the foundational framework for representing, analysing and even implementing a wide range of computational systems. The variety of logics available often allow us to characterise computational systems in a clear and concise manner, and such descriptions are then extremely useful as high-level abstractions of the original systems, particularly if the logics are amenable to proof or direct execution. Hence, part of our work involves devising logics that match our abstract intuition concerning specific computational systems.

Computation is, in turn, vital within logical systems, as a logical description is of little use unless we can actively do something with it. In particular, the two computational aspects of logic that we are mainly concerned with are verification and execution. Each of these utilises high-level logical descriptions in a fundamental way: verification techniques are used, for example, to check that a specific implementation satisfies a logical description or that a particular logical property holds within the description; meanwhile, rather than refining a logical description to gradually move towards a real implementation, it is possible to treat the logical description as the program and attempt direct execution of this description.

The development of increasingly complex contemporary systems has led to a resurgence of interest in this area, in particular the use of combinations of non-classical logics in order to provide high-level abstractions of dynamic, distributed, autonomous, and self-organising computational systems. Members of the Logic and Computation group are well known for their research activities across this area, specifically their work on logical reasoning, formal software development, and managing distributed computation.

Logical Reasoning

(Dixon, Fisher, Hustadt, Konev, Lisitsa, Wolter)

Members of the group have been instrumental in developing, and defining, research into reasoning techniques for temporal logics and multi-modal and description logics. Since the application of logical techniques within complex systems has shown the need for effective techniques for handling combinations of modal and temporal logics, work within the group has led to key results in this area. Work on logical reasoning has been strongly supported by EPSRC and by the CAPES funding agency (Brazil), and has involved collaboration with some of the internationally recognised leaders in the fields of automated reasoning, knowledge representation and theorem-proving.

Formal Software Development

(Dixon, Fisher, Hustadt, Malcolm)

The specification, verification and implementation of dynamic, distributed, autonomous, and self-organising computational systems involves techniques derived from many different areas. The group's activities in this area build on our foundational techniques, such as proof methods for combinations of logics, and develop formal methods for application to such complex systems. In particular, we have made key advances in algebraic specification, high-level programming languages, verification and testing, and the application of these techniques specifically to the formal development of agent-based systems. Work in this area has again been supported by EPSRC and by the British Council (Anglo-Dutch collaboration), and has involved collaboration with some of the internationally recognised leaders in the fields of formal methods, program verification and executable logics.

Managing Distributed Computation

(Dixon, Fisher, Hustadt, Lisitsa, Sazonov)

A particularly important area in which we are applying logical techniques is the use of software components for the management and organisation of distributed information and computation. The work of the group here covers the formalisation and implementation of Web-like databases, distributed/parallel proof techniques, high-level programming of dynamic groups, teams and organisations, and novel logical characterisations of distributed AI activity. In addition, this work has led to fundamental results in diverse areas, including hyperset theory. Work in this area has been supported by both EPSRC and Italian government funding, and has involved collaboration with some of the internationally recognised leaders in the fields of parallel processing, distributed information processing, and multi-agent systems.