If you would like to have a link to your Divisional reasoning
project inserted in the list below then please email to
the Director of the
Programme a one sentence description of your project
containing a link to a web page, ideally all as html source.
Reasoning Research Projects
Here are some links to research projects in the Division of
Informatics in the reasoning area.
- The Mathematical
Reasoning Group conducts research on all aspects of
mathematical reasoning, including automated and interactive
proof, theory formation, representation refinement and the
applications of mathematical reasoning to formal methods.
- Proof General
is a generic interface for proof assistants, currently based on Emacs
and supporting several provers, including Coq and Isabelle.
The aim of the Proof General project is to provide powerful and
configurable interfaces which help user-interaction with interactive
proof assistants. We are interested in developing generic
environments which support advanced features for proof
engineering, drawing on ideas from software engineering.
- The Mobile Resource Guarantees
project is building infrastructure for endowing mobile bytecode
programs with certificates as to their resource consumption, taking
the form of condensed formal proofs which can be checked by the
recipient before running the program.
- The Approximate and
Qualitative Reasoning Group carries out research on flexible and
dynamic knowledge modelling, structural and behavioural model-based
inference, and their applications (e.g. transparent fuzzy
classification, rough feature selection, and hybridised causal
explanation).
- The I-X: Intelligent
Technology research programme
is exploring representation and reasoning methods for a range of tasks
specially concerning
planning and activity
management. A particular concern is mixed-initiative reasoning
invoking collaborating human and system agents in a distributed environment.
- Prof
Keith Stenning My general interests are in how people use
communication to achieve their ends -- language (or diagrams)
as discourse (rather than structure). My current interests
centre on two areas: the comparison of modalities of
representation (e.g., language or graphics); and the
learning/teaching of formal knowledge, and its deployment in
context.
-
PropPlan is a planner based on propositional representations of planning problems,
these representations are themselves represented and manipulated using Binary
Decision Diagrams (BDDs).
PropPlan is written in StandardML, is compiled with PolyML under Linux, and uses David Long's
C-library, BDDLIB, to do most of its work.
Alan Bundy
4.2.04
