Organon VII - NIHIL NOVI

Výklad základů výrokové logiky, zejména její sémantiky, je standardní součástí kurzů logiky pro nejrůznější (nematematické a neinformatické) obory. Mnohé z významných pojmů a tvzení, s nimiž se student ve výkladu setká, mohou být zasazeny i do kontextu teoretické informatiky. Řadu objektů formální logiky lze vhodně reprezentovat prostředky diskrétní matematiky (např. stromy: formule, důkazy), některé otázky týkajících se sémantiky můžeme přeformulovat do řeči kombinatorického počítání. Cílem tohoto příspěvku je především poukázat na tyto souvislosti a "podívat se na elementární logiku očima diskrétní matematiky". Vše budeme demonstrovat na konkrétních příkladech, které se objevují snad ve všech základních kurzech.
Jakmile je na kurzu logiky vyložen pojem splnitelnosti a poté normálních forem, otevírá se široký prostor pro procvičování mnoha úloh algoritmického charakteru (úloha: je daná formule splnitelná?). Vznikají při tom přirozeně otázky, kdy je vhodnější použít metodu sémantických stromů, kdy stačí formuli "pouze prohlédnout" (zodpovědět otázku splnitelnosti "syntakticky") a kdy využívat tabulkovou metodu. Studenti mohou uvažovat nad tím, pro jaké třídy formulí lze problém splnitelnosti "rychle" rozhodnout. Odtud je již krok ke složitosti použitých algoritmů pro řešení problému splnitelnosti - na neformální úrovni. V příspěvku se dále podíváme na problém SAT, 3-SAT a 3-3SAT (a další) a na jejich vztahy. Převody mezi těmito problémy jsou zdrojem několika zajímavých otázek, které je vhodné na kurzech logiky zmínit a prezentovat při té příležitosti využití výrokové logiky v teoretické informatice. Poslední část příspěvku se věnuje otázce, jakým způsobem lze předestřené podněty organicky začlenit do základních kurzů logiky, případně jak by mohla vypadat osnova rozšiřujících cvičení k základnímu kurzu.