A proof assistant for first-order logic
Bachelor thesis assignment — 2017/18, Zoltán Onódy; supervisor Mgr. Ján Kľuka, PhD.
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 , sequent calculus , semantic tableaux , valuation tress , 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 ). 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.
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.
proof assistant, first-order logic, formalized mathematics, client-side web application
-  Barwise, J. (ed.) (1982): Handbook of Mathematical Logic. North Holland.
-  Smullyan, R.M. (1968): First-Order Logic. Springer.
-  Kľuka, J. (2011): Modulárne programovanie a verifikácia v druhorádovej aritmetike. Dizertačná práca. Univerzita Komenského.
-  Markus Wenzel, Freek Wiedijk (2002): A Comparison of Mizar and Isar. J. Autom. Reasoning 29(3–4): 389–411.
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
The current progress of proof assistant can be found at FMFI-UK-1-AIN-412/proof-assistant.
The last published version of thesis can be found here.
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
- 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.