**Keywords:** logic tools, first-order logic, client-side web application

Training and exercises are an important part of education process, especially when learning formalisms and constructs from logic such as formal proofs or semantics. For such exercises to be effective, the students need active feedback on what they are doing right or wrong. Interactive applications can make such feedback available even in the absence of teachers and thus allow students to work on the exercises according to their own time schedule.

The goal of this thesis is to create or extend tools that allow students to practise some of the tasks from logic courses: proofs, semantics tableaux or resolution. These shall be in the form of interactive, client-side web based applications.

J. Kľuka and J. Šiška, “Prednášky z matematiky (4) -logikypreinformatikov.”https://github.com/FMFI-UK-1-AIN-412/lpi/blob/master/docs/lecs/poznamky-z-prednasok.pdf, 2017. [Online;accessed 15-May-2018]. [1]

R. M. Smullyan,First-order logic [by] Raymond M. Smullyan. Springer-VerlagBerlin, New York [etc.], 1968. [2]

J. Kľuka and J. Šiška, “Tableau Editor.”https://github.com/FMFI-UK-1-AIN-412/tableauEditor, 2017. [Online; accessed 15-May-2018].[3]

E. Czaplicki, “Elm lang.”http://elm-lang.org/docs, 2012. [Online; accessed15-May-2018].[4]

J. Kľuka and J. Šiška, “Tableau Editor.”https://fmfi-uk-1-ain-412.github.io/tableauEditor/, 2017. [Online; accessed 15-May-2018].[5]

T. Bitai, “Ruzsa - Tableau Editor for Tarski‘s World.”https://ruzsa.tbitai.me//, 2017. [Online; accessed 15-May-2018].[6]

J. Komara, “Clausal Language- Programming Language and Proof Assistant.”http://ii.fmph.uniba.sk/cl/view/?lang=sk, 2016. [Online; accessed 15-May-2018].[7]

U. Stanford, “Fitch- application for constructing formal proofs in first-order logic.”https://ggweb.gradegrinder.net/support/manual/fitch, 2005. [Online; ac-cessed 15-May-2018].[8]

U. Stanford, “Boole- application for constructing truth tables.”https://ggweb.gradegrinder.net/support/manual/boole, 2005. [Online; accessed 15-May-2018].[9]

U. Stanford, “Tarski’s World.”https://ggweb.gradegrinder.net/support/manual/tarski, 2005. [Online; accessed 15-May-2018].[10]

M. Švaralová, “Výukový program demonštrujúci matematický princíp, bakalárskapráca,”FMFI UK, 2015.

- I ran module for testing and wrote some tests
- Fixed one/two bugs
- I ran modul for parsing formulas in the input, now remember the parsed formula in the app state. Parsing now works.
- I rewrote rendering of tableau using divs instead of table. I did some imperfect css styles.
- Show "Help" section.

- I fixed rendering of tableau using min-width and flexbox.
- I merged the rest of the functionality from the source tableau.
- I implemented Gamma and Delta To the model.
- Gamma and delta are rendered in tableau but not validated yet.

- I changed the structure of Substitution type.
- Implement proper rendering of gamma and delta substituting term and substituted variable.

- I implemented the functionality for substitution in exported module Formula. The first version of it.
- I implemented validation of gamma and delta rule.
- I wrote few tests to test this new functionlity.

- I implemented validation of new substituted variable in relation with existing bound/free variables.
- I wrote tests for Formula module.
- I created pull request in Formula module which is now hosted on faculty's github page.

- I implemented substitution in Formula module according supervisor's suggestions.
- I rewrote tests for substitution in Formula module.
- I implemented the refactored substitution in my tableau editor.

- I implemented prettify feature.
- I implemented adding node after every node.
- I implemented validation of delta.
- I refactored substitution according supervisor's review.
- Implemented exporting of tableau structure to json.

- Implemented deleting whole sub-tableau.
- Implemented deleting single node.
- Refactored adding new node wherever.
- Implemented switching beta subtrees.
- Refactored description of rules in Rules section.

- I implemented import of formulas from JSON.
- Undo, redo functionality.
- Showing errors also near the non-valid formula. Not only below the tablaeu.
- Better showing/hiding controls implementation.
- Implement nicer design.
- I reordered validation errors according to their importance.(gamma/delta)
- I divided validated case in Delta in two separated cases.(gamma/delta)
- Implemented changing of formula type.
- Wrote 3rd chapter of the thesis - Problem specification.

- Implemented last features and fixed last bugs.
- Wrote 4th chapter of the thesis - solution design.

- Refactored 4th chapter

- Refactored all of the errors in latex files.

- TODO