Automated Reasoning Research Area
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
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.
UK Conference of Professors and Heads of Computing
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),
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.
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
- 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.
Here we identify the impact of the Automated Reasoning research area
upon the seventeen
developed by the
Computer Science Research Strategy Group.
- 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.
- 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
- 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.
- 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.
- 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.
- 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
- 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
- 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.
- 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.
- 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
- 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
- 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
- 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
- In considering the Efficient Use of Scarce
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.
- 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.
- 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
- 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.
- Cambridge, University of
- Automated Reasoning Group,
- 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
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
- Oxford University
- Programming Research Group,
- 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,
- 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.
Forum of the Automated Reasoning Research Area
This document was generated using the
LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)
Copyright © 1993, 1994, 1995, 1996, 1997,
Computer Based Learning Unit, University of Leeds.
The command line arguments were:
latex2html -ps_images -no_navigation -split 0 -address Frisch@cs.york.ac.uk index.
The translation was initiated by Alan Frisch on 1999-07-22