Automatická verifikace důkazů v přirozeném jazyce
| Název práce v češtině: | Automatická verifikace důkazů v přirozeném jazyce |
|---|---|
| Název v anglickém jazyce: | Automated Verification of Natural Language Proofs |
| Klíčová slova: | Automatická verifikace|logika prvního řádu|dokazování matematických vět|přirozený jazyk |
| Klíčová slova anglicky: | Automated verification|first-order logic|theorem prover|natural language |
| Akademický rok vypsání: | 2020/2021 |
| Typ práce: | disertační práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra softwaru a výuky informatiky (32-KSVI) |
| Vedoucí / školitel: | doc. RNDr. Tomáš Dvořák, CSc. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 27.09.2021 |
| Datum zadání: | 27.09.2021 |
| Datum potvrzení stud. oddělením: | 27.09.2021 |
| Konzultanti: | RNDr. Martin Suda, Ph.D. |
| Zásady pro vypracování |
| 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. |
| Seznam odborné literatury |
| 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]. |
| Předběžná náplň práce |
| Automatická verifikace matematických důkazů, zapsaných v přirozeném jazyce, případně s omezenou gramatikou či slovníkem. |
| Předběžná náplň práce v anglickém jazyce |
| Automated verification of the correctness of mathematical proofs written in natural language, possibly with a restricted grammar or vocabulary. |