Web Forum

of the

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 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.

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.

- 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.

**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.

**British**

- Workshop on Automated Reasoning:
Bridging the Gap between Theory and Practice
- Practical Applications:
A group of conferences and exhibitions organised by
The Practical Applications Company
includes (often as part of The Practical Application Expo)
- The Practical Application of Constraint Technology Conference
- The Practical Application of PROLOG Conference
- The Practical Application of Intelligent Agents and Multi-Agents Conference
- The Practical Application of Knowledge Discovery and Data Mining Conference
- The Practical Application of Knowledge Management Conference

**European**

- European Workshop on Logics in Artificial Intelligence (JELIA)
- European Summer School in Logic, Language and Information (ESSLI)

**International**

- International Conference on Computational Logic (CL)
- International Conference on
Automated Deduction (CADE)
- International Conference on Principles of
Knowledge Representation and Reasoning (KR)
- IEEE Symposium on Logic in Computer Science (LICS)
- Conference on Rewriting Techniques and Applications (RTA)
- Computer-Aided Verification (CAV)
- International Workshop on Frontiers of Combining Systems
- International Workshop on Unification
- International Conference on
Automated Reasoning with
Analytic Tableaux and Related Methods (TABLEAUX)
- International Workshop on First
Order Theorem Proving (FTP)
- International Conference on Theorem Proving
in Higher Order Logics (TPHOLs)
- International Workshop on Nonmonotonic
Reasoning (NM)
- International Workshop on Desription
Logics (DL)
- International Conference on Principles and
Practice of Constraint Programming (CP)
- Theoretical Aspects of Rationality and Knowledge (TARK)
- International Workshop on Logic-Based Program
Synthesis and Transformation (LOPSTR)
- Iternational Workshop on Higher-Order Algebra, Logic, and Term
Rewriting (HOA)
- Knowledge Representation Meets Databases (KRDB)

*Artificial Intelligence**Computational Intelligence**Constraints**Journal of Artificial Intelligence Research**Journal of Automated Reasoning**Journal of Logic, Language and Information*

Publisher's home page

Organisational home page*Journal of Logic and Computation*

(There is also a hypertext bibliography for this journal.)*Journal of Symbolic Computation**Logic Journal of the IGPL*

**British**

- Society for the Study of Artificial Intelligence
and the Simulation of Behaviour
- Scottish Theorem Proving: Hosts the
peripatetic Scottish Theorem Proving Seminar Series.
- Temporal Reasoning, Artificial
Intelligence and Logic (TRAIL) Group: An informal group of
researchers which holds occasional seminars on topics related to
Temporal Reasoning, Reasoning about Actions,
Artificial Intelligence and Logic.

**European**

- Compulog: The European Network of Excellence in
Computational Logic
- European Association for Logic,
Language and Information

**International**

- The Automated Mathematical Induction
pages
are devoted to automated proof by induction and are
maintained by David McAllester.
- The Research Sites
pages of Thomas Uribe contain pointers to collections of papers and
FTP sites focused on automated deduction.
- The Mechanized Reasoning
pages are devoted to automated deduction and
maintained by Michael Kohlhase and Carolyn Talcott.
- The Reasoning about Actions
pages are maintained by Rob Miller.
- Satisfiability Library.
- Colibri
is an electronic newsletter and WWW service aimed at people
interested in the fields of natural language processing, speech
processing and/or logic.
- List of
Related Conferences and other Events
maintained by the
*Logic Journal of the IGPL*. - List of
Logic Related Conferences
maintained by the Symposium on Logic in Computer Science.

This document was generated using the
**LaTeX**2`HTML` translator Version 98.1p1 release (March 2nd, 1998)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, 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

Frisch@cs.york.ac.uk