Web Forum

of the

Automated Reasoning Research Area

Edited by Alan Bundy, Michael Fisher and Alan Frisch

This draft web page is being brought to the attention of the UK automated reasoning community to solicit input and comment. The intention is that by the end of April there will be a web-based system to facilitate electronic discussion of the contents of this page. At that point the availability of this page and the associated discussion forum will be broadly announced.
The editors would be grateful for any feedback on the page, but we are particularly looking for the following:
1. Constructive criticisms and suggestions on our draft attempt to link automated reasoning to the Generic Questions.
2. The URL of your automated reasoning group so we can link to it plus a few key words describing your group's research interests. If you do not yet have a group web page then we strongly urge you to create one as soon as possible.
This is an excellent opportunity for the automated reasoning community to promote itself. We expect to be one of the first research areas to be linked to the Web Forum.

The UK Conference of Professors and Heads of Computing founded the Research Strategy Group (RSG) to promote UK computer science research to outside bodies, such as funding agencies and the government. As part of its brief RSG is developing a Web Forum on computer science research.

This forum includes, for instance, a list of Generic Questions (GQs), which research in computer science is addressing (and will continue to address for the foreseeable future). The generic questions provide a link between information technology products and research areas. This page attempts to explain how automated reasoning addresses these generic questions. It also provides pointers to many of the major UK research groups in automated reasoning.

What is Automated Reasoning?

The automated reasoning research area is the area of computer science that studies reasoning processes as computational processes. The computational systems of primary concern reason about their domain of interest by manipulating statements that describe that domain.

This use of declarative knowledge promotes generality in system design; a system that reasons about one domain can be converted to another domain by modifying the declarative knowledge, and reasoning processes can be developed independently of the domain.

Research in this area is concerned with all phases of the development of automated reasoning systems:

problem formulation,
system design, and
system analysis and evaluation.

The area of automated reasoning covers a diverse range of topics. Among its subareas are those that are concerned with particular computational techniques for automating reasoning, including:

equational reasoning and rewriting;
unification and constraint solving;
deductive and non-deductive reasoning, including abduction, induction, nonmonotonic reasoning, and analogical reasoning; common sense reasoning;
a range of topics that fall under the heading of knowledge representation and reasoning;
model checking; and
theorem proving.

Other subareas are concerned with particular applications of automated reasoning:

for programming, especially logic and functional programming;
for databases, especially deductive databases;
the application of formal methods to specifying, synthesising, transforming and proving properties of computer systems, particularly those for which safety and security are critical; and
for reasoning about mathematics.

Relationship of Research Area to Generic Questions

Here we identify the impact of the Automated Reasoning research area upon the seventeen Generic Questions developed by the Computer Science Research Strategy Group.

1.: In Understanding the Impact of IT, models of societal interactions may be used, and simulations of complex psychological and social patterns may be developed. In both these cases, Automated Reasoning can be used to model widespread effects of particular IT elements.
2.: When considering mechanisms for Managing Complexity of Real World Systems, Formal Methods, and hence Automated Reasoning, have a role in proving properties of simulation models, etc. Automated Reasoning may also have a role in building such models, especially where algorithmic solutions are not available but inference is possible. Automated Reasoning may also be used in machine assistance for building simulation models, e.g. via direct synthesis of components, for assessing the coherence of a particular combination of components, and for analysing the results of large simulations.
3.: Similar remarks to the previous question can be made about Managing Complexity of Computer Systems, but with additional strength since Automated Reasoning is commonly used for manipulating models of computer systems, e.g. process algebras for modelling concurrent systems and temporal logics for describing hardware.
4.: Automated Reasoning is a major technology for building Smarter Products, Systems and Services, e.g., if they need to reason about the task under consideration, the methods of solution, the environment, etc. Reasoning itself is closely linked to many notions of `intelligence'. Automated Reasoning is also used to reason about the logical representations of intelligent systems.
5.: Automated Reasoning has a major role to play in supporting the design, maintenance and verification/validation of computer systems. Hence, it is a key aspect of Cost Effective Computing. Automated Reasoning techniques can also be used directly in systems, for instance, especially where the cost bottleneck is design rather than efficiency of the final system. Automated Reasoning may enable rapid design, e.g. by posing the task as constraint-based search, rather than specification of an algorithm, or by synthesising programs directly from high-level specifications. Finally, during the design phase, Automated Reasoning can be used to assess the potential efficiency of alternative designs paths.
6.: In the areas of Human Interactions, Communications and Collaborations, Automated Reasoning has a central role to play in the design of intelligent agents and artificial organisations, e.g. via planning technologies, and interface, workflow and process modelling.
7.: Automated Reasoning plays a significant part in improving Ease of Use, for example, by providing much of the reasoning technology underlying speech and language processing, software and interface agents, and powerful extensions of knowledge and databases, and by supporting the design and reasoning about programming languages.
8.: Concerning Integration and Interoperability, Automated Reasoning has a role in the specification of systems and the reasoning required to match components via their specification. In addition, the interoperability of software components may be dependent on the justification of their faithfulness, which can again be established (dynamically in some cases) using Automated Reasoning techniques.
9.: In establishing the Safety, Reliability and Predictability of complex systems, formal verification using Automated Reasoning techniques is widely used. For example, Automated Reasoning tools have been used in the verification of hardware (e.g. microprocessors), manufacturing and control systems (e.g. flight control), and distributed software (e.g. network protocols). Thus, Automated Reasoning has a major role in satisfying the proof obligations arising from the use of formal methods in safe system design.
10.: Automated Reasoning is a key component in establishing both Security and Integrity For example, the formal representation of network protocols allows Automated Reasoning techniques to be used to verify the properties of such communication. With the increasing use of ``plug and play'' solutions and mobile programs, there is a need to utilise Automated Reasoning tools in order to check that these elements do not violate the integrity of the system when incorporated.
11.: Concerning Access and Interpretation, Automated Reasoning has a major role to play in bridging the gap between knowledge sources and specific queries and data. Inference can be used to translate between knowledge representations and to derive implicit knowledge from that explicitly stored. Examples include the use of learning techniques in data-mining, and the use of agents for information retrieval where the agents incorporate refined Automated Reasoning techniques.
12.: Automated Reasoning has a role in Evolution, Flexibility and Maintenance, for example via formal techniques for re-synthesising a program from a modified specification via a proof that the specification is realisable. With the advent of more dynamic and adaptable systems, the run-time assessment of new modifications is also desirable.
13.: Automated Reasoning may be used for Scalability and Distribution, for example via formal techniques for specifying components of a distributed system and satisfying proof obligations that arise from matching specifications of components. It may also be used in the design of programming languages which support parallelism and distribution, and in the development of appropriate communication protocols.
14.: In considering the Efficient Use of Scarce Resources, Automated Reasoning can be used for both design and configuration problems. As a software design is refined, the resource implications for alternative design options can be evaluated using Automated Reasoning techniques.
15.: Automated Reasoning can be used to model distributed systems with Emergent Behaviour and to reason about the change in behaviour within such systems. In particular, given a formal model of the dynamics of a system, such techniques can be used to examine the possible future development of the system's behaviour.
16.: Automated Reasoning an important ingredient of almost any intelligent system and is closely related to the question What is Mind?. In addition, the space of mechanisms it provides are candidate cognitive models. In many simulations of aspects of mind, Automated Reasoning techniques are utilised to represent higher-level functions, particularly those concerned with reasoning. In addition, Automated Reasoning techniques are central to many endeavours concerned with the development of artificial intelligence.
17.: Automated Reasoning has been drawn on in various ways to provide models of Computation and Information. Consider, for instance, evaluation of lambda calculus terms as a model of functional programming; and resolution applied to Horn clauses as a model for logic programming.

Automated Reasoning Research Groups in the UK

Cambridge, University of

Automated Reasoning Group, Computer Laboratory.

Durham, University of

Computer-Assisted Reasoning Group, Department of Computer Science: Research on computer-assisted formal reasoning, functional programming, and formal methods. One of the strong theoretical underpinnings for the work is type theory and logic. Current research projects include: theory and application of coercive subtyping, strong functional programming with dependent types, the Plastic proof checker based on type theory, mathematical vernacular and linguistic semantics, and model checking and verification of concurrent programs

Edinburgh, University of

Mathematical Reasoning Group, Department of AI: Work on the automation of all aspects of mathematical reasoning, including: proving theorems, explaining proofs, formalising informal problems, learning new proof methods, forming concepts, conjecturing theorems, etc. Most of their recent work has been on the automation of inductive inference and its application to formal methods. The Group also occasionally strays outside mathematics and formal methods to game playing (bridge, go), uncertainty and configuration problems.

Essex, University of

Constraint Programming Group, Department of Computer Science.

Glasgow, University of

Formal Methods and Theory Research Group, and the informal Glasgow Provers Group.

Heriot Watt University

Dependable Systems Group, Department of Computing and Eletrical Engineering: Provides a forum for research into improving the reliability and predictability of computer systems through the application of rigorous design and implementation techniques. The Group's research interests encompass program proof and transformation, performance modelling and simulation, and functional prototyping for parallel systems.

Imperial College of Science, Medicine and Technology

Logic and Automated Reasoning Section, Department of Computing.

Leeds, University of

Automated Reasoning Group, School of Computer Studies.

Algorithms, Problems, Empirical Studies (APES) Group Group, School of Computer Studies: See entry under ``Strathclyde, University of''.

Manchester Metropolitan University

Logic and Computation Group, Department of Computing and Mathematics: Principal interests involve agents, proof methods and programming languages. Within the area of automated reasoning the Group's research concerns non-classical logics, particularly proof methods (mainly resolution-based) for modal, temporal and multi-modal logics.

Oxford University

Programming Research Group, Computing Laboratory.

Queen Mary and Wesfield College

Artificial Intelligence Research Group, Department of Computing Science.

St. Andrews, University of

Theoretical Computer Science Group, School of Mathematical and Computational Science.

Strathclyde, University of

Algorithms, Problems and Empirical Studies (APES) Group, Department of Computer Science: An informal group of researchers at the University of Leeds and Strathcylde studying search algorithms and problems through large scale empirical studies. Within the area of automated reasoning, the Group has expertise in the design and analysis of algorithms for constraint satisfaction, and satisfiability. Key words: constraint satisfaction, satisfiability, search, NP-complete problems.

York, University of

Intelligent Systems Group, Department of Computer Science: Research concerned with the theoretical principles of artificial intelligence and their application to real-world domains. The Group's research focuses on three core areas of artificial intelligence-knowledge representation and reasoning, machine learning and natural language processing-though most of the Group's projects span these areas.