A proof assistant for first-order logic

Bachelor thesis assignment — 2017/18, Zoltán Onódy; supervisor Mgr. Ján Kľuka, PhD.

Presentation

https://docs.google.com/presentation/d/1Oh5hlx_QH-K8jdsZfxtkSUjox3CQ_CVEoIMELoCDEzM/edit?usp=sharing

Annotation

The learning outcomes of mathematics courses at our faculty include acquisition of the mathematical style of writing and reasoning. Achieving this goal requires exercises in formulating definitions, propositions, and proofs with timely feedback. Mathematical language and reasoning use established constructs whose theoretical models are the language of first-order logic and formal systems of axioms and derivation rules (Hilbert calculus [1], sequent calculus [1], semantic tableaux [2], valuation tress [3], etc.). There are, however, also practical software systems for composition of theories and proofs in readable formal languages similar to the language of mathematical writing, and for intelligent automated checking of proofs written in these languages (Mizar, Isabelle/Isar [4]). Their use in teaching practice is, however, discouraged by the need to learn the formal language, the mode of interaction with the software, opaque proof checking (it is not quite clear which leaps of thought the machine accepts and why), and the need to install software. We thus aim at developing a web-based environment for development of theories and interactive composition of proofs from derivation rules expressed in natural language with easily understandable verification of correctness of each proof step.

Goals

The goal of the thesis is to design, implement, and test a prototype interactive assistant for composition of proofs of propositions in first-order logic as described in Annotation. Correctness will be ensured by basing the design on a selected suitable formal system [1, 2, 3]. The assistant should then be incorporated into a development environment allowing to specify the language and axioms of a theory and state and prove propositions, using earlier-proved propositions as lemmata. The implementation will use client-side web technologies in order to facilitate deployment.

Keywords

proof assistant, first-order logic, formalized mathematics, client-side web application

References


Expected Progress

the 18th of November

the 15th of December

the 30th of December

the 10th of January

the 7th of February

the 28th of February

the 30th of March

the 30th of April


Presentation of references

https://docs.google.com/presentation/d/1dp-STFTT7HmmyysMuF1Dmc-S8OWZwjHJJulp2_CZgoI/edit?usp=sharing


Source code

The current progress of proof assistant can be found at FMFI-UK-1-AIN-412/proof-assistant.

Thesis

The last published version of thesis can be found here.

Diary

February 19 - 25

February 26 - March 04

March 05 - 11

March 12 - 17

March 18 - 25

March 26 - April 01

April 02 - April 08

April 09 - April 16

April 16 - April 22

April 23 - April 29

May 21 - May 27