Research Project
Computer-Assisted Reasoning with Natural Language:
Implementing a Mathematical Vernacular
R. Garigliano
and
Zhaohui Luo (with thanks to S. Shiu)
Dept of Computer Science, University of Durham
Funded by Leverhulme Trust (Jan 1997 -- Dec 1998).
We believe that vigorous inter-disciplinary research in the theory and
technology of Computer-Assisted Formal Reasoning (CAFR) and Natural
Language Processing (NLP), will result in important developments in
the technology and logical foundation of computer-assisted reasoning.
Our long term aim is to develop the theory and techniques with which
the complementary powers of NLP and CAFR can be combined to support
computer-assisted reasoning. The current project is to address this
in the context of mathematical reasoning, where the language used is
precise and there are fewer problems with inherent ambiguity, but it
still has its own interesting linguistic problems. We shall study and
develop theory and techniques based on type theory for implementing
proof systems that assist mathematicians to reason in their own
mathematical vernacular, that is, a mathematical and natural language
suitable for ordinary mathematical practice and implementable based on
a formal theory.
In this project, we shall first focus our research on development of a
suitable type-theoretic semantics for mathematical reasoning in
natural language. On the basis of the semantics, we shall study the
techniques to implement a mathematical vernacular. Our major
objective is to develop a useful and implementable type-theoretic
foundation for computer-assisted reasoning with natural languages. A
successful development of a mathematical reasoning system will be
viewed as a justification of the theory.
Related personnel
- Paul Callaghan
(research fellow).
- Simon Shiu (PhD student, graduated 1997, now working for Hewlett Packard).
Zhaohui.Luo at rhul.ac.uk