ATTENTION/WARNING - NE PAS DÉPOSER ICI/DO NOT SUBMIT HERE

Ceci est la version de TEST de DIAL.mem. Veuillez ne pas soumettre votre mémoire sur ce site mais bien à l'URL suivante: 'https://thesis.dial.uclouvain.be'.
This is the TEST version of DIAL.mem. Please use the following URL to submit your master thesis: 'https://thesis.dial.uclouvain.be'.
 

Proof of concept of an interactive theorem prover system using natural language input

Zarza Davila, Andres
(2021)

Files

ZarzaDavila_14781600_2021.pdf
  • Open access
  • Adobe PDF
  • 1.62 MB
Download

Details

Supervisors
Glineur, François
Degree label
Master [120] : ingénieur civil en science des données, à finalité spécialisée
Abstract
This work presents a proof of concept for a mathematical proof system that would allow users to write in a close to natural language while generating proofs that are machine verifiable. The main objective is to assess the feasibility and features of such a project and explore promising leads to this end. The current implementation is a web application written in Python/Javascript with backend in Django and frontend in React. It constructs and verifies proofs with Lean, an interactive theorem prover. Natural language processing is made by simple pattern matching. The current implementation is still somehow limited but allows to envision a more advanced system. The last chapter develops possible ideas to further improve and extend the current proof of concept.