Automatická verifikace důkazů v přirozeném jazyce
| Thesis title in Czech: | Automatická verifikace důkazů v přirozeném jazyce |
|---|---|
| Thesis title in English: | Automated Verification of Natural Language Proofs |
| Key words: | Automatická verifikace|logika prvního řádu|dokazování matematických vět|přirozený jazyk |
| English key words: | Automated verification|first-order logic|theorem prover|natural language |
| Academic year of topic announcement: | 2020/2021 |
| Thesis type: | dissertation |
| Thesis language: | čeština |
| Department: | Department of Software and Computer Science Education (32-KSVI) |
| Supervisor: | doc. RNDr. Tomáš Dvořák, CSc. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 27.09.2021 |
| Date of assignment: | 27.09.2021 |
| Confirmed by Study dept. on: | 27.09.2021 |
| Advisors: | RNDr. Martin Suda, Ph.D. |
| Guidelines |
| The student will work on the problem of automatically verifying the correctness of mathematical proofs written in natural language, possibly with a restricted grammar or vocabulary. He will investigate extensions of first-order logic for representing mathematical statements in a theorem prover, as well as algorithms and heuristics that can generate formal proofs in a natural deduction style. He will build an implementation of these ideas and use it to verify a series of proofs in set theory, number theory, combinatorics and/or other mathematical domains. |
| References |
| Grzegorz Bancerek, Czesław Byliński, Adam Grabowski et al. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. J. Autom. Reasoning 61 (2018), 9-32.
Maximilian Doré, Krysia Broda. Intuitive Reasoning in Formalized Mathematics with ELFE. Commun. Comput. Inf. Sci. 1022 (2019), 549-571. Steffen Frerix, Peter Koepke. Automatic Proof-Checking of Ordinary Mathematical Texts. Conference on Intelligent Computer Mathematics (CICM 2018), CEUR Workshop Proceedings 2307 (2018). John Harrison. Handbook of practical logic and automated reasoning. Cambridge University Press, 2009. John Harrison, Josef Urban, Freek Wiedijk. History of interactive theorem proving. Handbook of the History of Logic 9 (2014), 135–214. Cezary Kaliszyk, Florian Rabe. A Survey of Languages for Formalizing Mathematics. Lecture Notes in Artificial Intelligence 12236 (2020), 138-156. M. Saqib Nawaz, Moin Malik, Yi Li, Meng Sun and M. Ikram Ullah Lali, A Survey on Theorem Provers in Formal Methods. arXiv:1912.03028 [cs.SE]. |
| Preliminary scope of work |
| Automatická verifikace matematických důkazů, zapsaných v přirozeném jazyce, případně s omezenou gramatikou či slovníkem. |
| Preliminary scope of work in English |
| Automated verification of the correctness of mathematical proofs written in natural language, possibly with a restricted grammar or vocabulary. |