University students often struggle to master mathematical style of reasoning. In order to alleviate this problem, we have decided to build an interactive, web-based proof assistant. Our proof assistant supports three types of proofs: direct proof, proof by cases, and proof by contradiction. The proof is built primarily by chaining claims. The proof assistant checks whether a new claim logically follows from previous claims by some sound basic rule of inference known to it. This should allow students to focus on intuitively determining logical consequences rather than on finding or blindly trying inference rules. The user writes the claims as first-order formulas. The proof assistant is based on a hybrid formal proof system mixing Hilbert calculus and Sequent calculus. The proof assistant also implements many common additional sound rules of inference. The application has been implemented in the functional programming language Elm. It is a working prototype and we expect further development of the project in the future. The ease of interaction with the proof assistant was tested by students who gave us positive and informative feedback some of which we have implemented.

Študenti na univerzite majú často problémy osvojiť si matematický štýl uvažovania. Na zmiernenie tohto problému sme sa rozhodli vytvoriť interaktívny webový dokazovací asistent. Náš dokazovací asistent podporuje tri typy dôkazov: priamy dôkaz, dôkaz analýzou prípadov a dôkaz sporom. Dôkaz je predovšetkým založený na reťazení tvrdení. Dokazovací asistent overuje, či nové tvrdenia sú logickými dôsledkami predchádzajúcich tvrdení a nejakého inferenčného pravidla, ktoré asistent pozná. To by malo študentom umožniť sústrediť sa na dôkaz samotný namiesto nepremysleného skúšania inferenčných pravidiel. Používateľ do asistenta píše sformalizované prvorádové formuly. Dokazovací asistent je postavený nad hybridným formálnym systémom pozostávajúcim z hilbertovského a sekventového kalkulu a pozná aj ďalšie korektné inferenčné pravidlá. Asistent bol naprogramovaný vo funkcionálnom programovacom jazyku Elm. Je funkčným prototypom, ktorý sa bude v budúcnosti ďalej vyvíjať. Jednoduchosť používania sme testovali so študentmi. Tí nám poskytli pozitívnu a~informatívnu spätnú väzbu, ktorú sme čiastočne zapracovali.