School of Computer Science



This grouping includes research on various forms of reasoning, including theorem proving and uncertain reasoning, with particular application to mathematical knowledge management, mathematical document recognition, computer algebra, natural language processing, and multi-attribute and multi-agent decision-making. The research is relevant both to understanding how human reasoning works and to designing useful practical tools.

Theorem Proving, Proof Planning and Symbolic Algebra

In the theorem-proving area we investigate different approaches such as proof planning, learning of methods, agent-oriented theorem proving, theorem proving with partiality, and integration of theorem proving and computer algebra. One particular focus is on reasoning in mathematical domains. Improvements in the usability of automated deduction systems have been made by flexibly combining heterogeneous methods (e.g., mathematical processing and novel higher-order methods); by extending and combining traditional reasoning techniques into novel explorative approaches to generate new mathematical theorems; and by facilitating the application of human-understandable strategies and notations. We have also demonstrated the crucial importance of the particular representations used.

Collaborations based on the theorem-proving work include participation in Calculemus and the MKM network

Natural Language Processing, Uncertain Reasoning and Decision-Making

Part of our work on natural language processing is on pragmatic reasoning processes needed in handling the beliefs of discourse participants and in understanding metaphorical utterances. The reasoning processes developed here thoroughly integrate multi-context and qualitatively uncertain and vague reasoning. Pleae see the Natural Language Processing Group for more.

Other work on uncertain reasoning includes research on improved axiom systems for prioritised fuzzy constraint satisfaction problems, theoretical analysis of how to make heterogeneous uncertain reasoning agents understand each other during cooperation, and the management of resource constraints under uncertainty in robot planning applied to real-world problems (such as space exploration).

Research on decision-making includes work on integrating diverse negotiation methods (interest-exploring, tradeoff, arguing by reward, concession, etc.) and on improved and mathematically well-founded attribute-aggregation operators in multi-attribute decision making.


For the work mentioned just above on robot planning and other work on that topic please see Robotics and Cognitive Architectures Group.

Scientific Document Analysis and Symbolic Algebra

The Scientific Document Analysis Group works on the recognition, analysis and enhancement of optically scanned or digitally born documents. We work primarily on scientific documents but also on historical or technical documents.

Our core activities centre on the recognition of mathematical formulae and scientific diagrams and the semantic analysis of recognition results to correct recognition errors and improve interoperability with scientific and mathematical software. The group therefore also investigates representation issues of concepts, as they appear in mathematical writing, in symbolic computation and reasoning systems.

Document enhancement activities we are pursuing include enabling scientific documents for the visually impaired, and metadata extraction and correction to improve search abilities on target documents.

Main Academic Staff