# 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

- [1] Barwise, J. (ed.) (1982): Handbook of Mathematical Logic. North Holland.
- [2] Smullyan, R.M. (1968): First-Order Logic. Springer.
- [3] Kľuka, J. (2011): Modulárne programovanie a verifikácia v druhorádovej aritmetike. Dizertačná práca. Univerzita Komenského.
- [4] Markus Wenzel, Freek Wiedijk (2002): A Comparison of Mizar and Isar. J. Autom. Reasoning 29(3–4): 389–411.

## Expected Progress

the 18th of November

- I know how to use ELM

the 15th of December

- the Data Structure has been created for standard proofs
- a simple GUI, where we will be able to work with the created structure

the 30th of December

- working prototype where we can do at least one proof

the 10th of January

- the intro chapter is written

the 7th of February

- we support multiple definitions and multiple claim

the 28th of February

- proofs with definitions of Inference and Satisfiability

the 30th of March

- fully functioning proof assistant

the 30th of April

- bachelor thesis is finished

## 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

- I extracted the Formula parser from tableau editor and published it on elm packages. http://package.elm-lang.org/packages/ZoltanOnody/tablueau-parser/1.0.0/Formula

### February 26 - March 04

- Design prototype of the proof assistant
- Implement simple API for the editor

### March 05 - 11

- Reimplement the project structure so it matches more the final design

### March 12 - 17

- Hopefully final structure reimplementation (after CR)
- Add very simple formula matcher

### March 18 - 25

- Move formula parser to new repo (under FMFI-UK-1-AIN-412 account)
- Discuss the current implementation and agree on the next steps

### March 26 - April 01

- Change the implemntation according to disscussion from last week

### April 02 - April 08

- Easter [netflix & chill]

### April 09 - April 16

- https://docs.google.com/presentation/d/1YZozWXIlqu1voye6eMNKfM2JGrW9SuUBqIYWEii2-hs/edit?usp=sharing
- Discuss and come up with a first order logic implementation of the proof assistant
- Finish propositional calculus

### April 16 - April 22

- Finish first order logic
- Write curicullum for bachelor thesis

### April 23 - April 29

- Starting to write the bachelor thesis

## May 21 - May 27

- Realising I started to write the thesis too late.