Towards a user-friendly natural language proof assistant - The outline of a system that can be used to implement applications that enable non-expert users to construct computer-verified natural language arguments

Abstract

In more or less any discussion, however consequential, it is left for the participants to work out in their own head whether the arguments necessitate the conclusions put forward, or are lacking or flawed. When the discussion concerns philosophical or real-world issues there are no good alternatives for people who want to formalize their arguments and have them verified by a computer.

Proof assistants can be used construct computer-verified arguments about mathematical issues, but for all existing proof assistants a high level of expertise is needed to be able to construct proofs or understand them.

This thesis outlines the architecture of a system that could be used to implement a proof assistant that lets non-expert users construct computer-verified arguments in natural language, about more or less any topic that can be described explicitly using natural language sentences. The system described could potentially be used for other things as well, including but not limited to uses within the fields of knowledge representation and translation.