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

Zhaohui.Luo at rhul.ac.uk