Zadání studentských prací

Zadání bakalářské práce

Základní údaje

Posluchač:
Program / Obor:

Název (CZ):	Strojové ověření konstruktivního důkazu úplnosti klasické výrokové logiky
Název (EN):	Automated proof-checking of the constructive proof of completeness of classical logic

1.	Seznámit se s klasickou výrokovou logikou [1] - syntax, sémantika, věta o úplnosti (konstruktivní verze).
2.	Seznámit se s principy konstruktivní matematiky (intuicionistická logika) [2].
3.	Nastudovat základy teorie typů jako alternativního nástroje pro základy matematiky [3].
4.	Seznámit se se systémy pro strojové ověřování důkazů [6], zejména s novým programem s názvem Lean [4].
5.	Formalizace důkazu úplnosti klasické logiky v Leanu s cílem, aby dané strojové ověření bylo vhodné k modifikaci pro další neklasické logiky (zejména Lukasiewiczovu [5]).
6.	Publikace formalizovaného důkazu na příslušném fóru.
7.	Sepsání práce v LaTeXu.
8.

Vyžadovaný formát referencí

Dodržujte následující formátování seznamu použité literatury. Pokud formát nedodržíte, bude Vám zadání vráceno k přepracování.

článek v časopise: Autor/ři, Název_článku. Název_časopisu ročník, rok, stránky.
příklad: K. G. Hare, Tiles in quasicrystals with quartic irrationality. Mathematics of Computation 75, 2009, 405–420.
kniha: Autor/ři, Název_knihy. Vydavatel, rok.
příklad: N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous univariate distributions. John Wiley & Sons, New York, 1994.
příspěvek ve sborníku: Autor/ři, Název_příspěvku. In ‘Název_sborníku’, Vydavatel, rok, stránky.
příklad P. Mueller, P. Wonka, S. Haegler, et al., Procedural modeling of buildings. In ‘ACM SIGGRAPH 2006 Papers’, ACM New York, 2006, 614–623.

1.	V. Švejdar, Logika - neúplnost, složitost a nutnost. ACADEMIA, Praha, 2002.
2.	A. S. Troelstra, D. van Dalen, Constructivism in mathematics, an introduction. Elsevier Science, Amsterdam, 1988.
3.	P. Martin-Lof, Intuitionistics type theory, volume 1 of Studies in Proof Theory. Bibliopolis, Neapol, 1984.
4.	J. Avigad, L. de Moura, S. Kong, Theorem Proving in Lean. Online tutorial: \url{https://leanprover.github.io/theorem\_proving\_in\_lean}
5.	P. Fejl, Moderní čtení Rose-Rosserova důkazu úplnosti Lukasiewiczovy logiky. Bakalářská práce, FJFI ČVUT v Praze, Praha, 2017.
6.	\url{https://en.wikipedia.org/wiki/Automated\_proof\_checking}

Školitel:
	(Celé jméno a příjmení s tituly)
Pracoviště:	Ústav teorie informace a automatizace AV ČR, v.v.i. Pod Vodárenskou věží 4 182 08 Praha 8, Česká Republika
	(Název instituce a adresa)
Email:
Telefon:

Konzultant:
	(Celé jméno a příjmení s tituly)
Pracoviště:
	(Název instituce a adresa)

Datum zadání:
Datum odevzdání:

Stav zadání

Schváleno KM

Historie

2017-10-16 20:54:25

– zahájení procesu zadání

2017-10-16 21:48:29

– zasláno školiteli

2017-10-19 21:17:13

– upraveno školitelem

2017-10-20 18:00:15

– zasláno na KM

2017-10-20 18:28:49

– žádost o autorizaci

2017-10-21 07:58:02

– autorizováno školitelem

2017-11-09 10:51:22

– schváleno KM

2019-01-09 21:12:07

– reaktivováno

2019-01-10 11:30:12

– vráceno k opravě

2019-01-16 10:50:51

– zasláno školiteli

2019-01-17 16:48:34

– upraveno školitelem

2019-01-21 09:51:39

– zasláno na KM

2019-01-30 13:32:53

– vráceno k opravě

2019-02-05 17:26:01

– zasláno na KM

2019-02-19 13:02:09

– schváleno KM