Přirozená dedukce vs. sémantická tabla …:

Rezoluční metoda pro výuku dedukce

Mgr. Martina ČÍHALOVÁ
Katedra informatiky, VŠB-TU v Ostravě
m.tina.cihal@gmail.com



Abstrakt

Cílem příspěvku je navržení didakticky vhodného přístupu k výuce dedukce pomocí rezoluční metody. Výhodou je jednoduchá automatizovatelnost postupu, a tedy i poměrně jednoduchá kontrola jeho správnosti pedagogem. Rezoluční metodu lze aplikovat pouze na formule ve speciálním tvaru, tzv. klauzulární (Skolemově) formě. V příspěvku se zabýváme především analýzou a návrhem automatizovaného postupu určení složitosti úloh pro převedení formule do Skolemovy klauzulární formy, tj. skolemizací. Skolemizace patří k obtížnější látce probírané v kurzu Matematická Logika a je velice žádoucí, aby pedagog při výběru příkladů z databáze mohl dopředu zjistit, jak je daná úloha náročná na vyřešení. Na úvod je vhodné vybírat pro studenty jednodušší příklady, kdy formule není příliš dlouhá a při skolemizaci je na formuli aplikováno jen několik málo kroků algoritmu skolemizace. Další výhoda určení složitosti formule je při tvorbě zápočtových a zkouškových písemek, kdy je možné vytvořit více variant se stejnou obtížností. Různé formule se však vzájemně liší nejen složitostí spočívající v aplikaci konkrétních kroků algoritmu, ale složitost úlohy určuje rovněž syntaktická struktura formule, zejména její hierarchický řád. Navrhli jsme konečný počet vzorů, kde u každého je určen typ složitosti (jak syntaktické hierarchie, tak i složitost aplikace algoritmu skolemizace). Z didaktického hlediska nemá smysl vytvářet složité vzory, neboť student s rostoucím počtem závorek a délkou formule ztrácí nad příkladem nadhled a chyby v jednotlivých krocích algoritmu skolemizace nejsou dány jeho neznalostí, ale špatnou orientací ve struktuře formule. Námi navržený software pro výuku umožňuje vybrat formuli konkrétní složitosti jak podle použitých kroků algoritmu, tak podle její syntaktické struktury dané hierarchickým řádem. Dalším krokem rezoluční důkazové metody je unifikace literálů a uplatňování rezolučního pravidla. Zde se využije osvědčený Robinsonův algoritmus unifikace s tím, že do příslušných typů vzorů přidáme složitost příslušné potřebné unifikace. Tímto způsobem se provede celý důkaz rezoluční metodou, který bude snadno kontrolovatelný na správnost postupu, a systém zároveň studenta důkazem povede krok po kroku tak, aby student pochopil, kde dělá chyby a proč jsou jednotlivé kroky prováděny právě tak, jak jsou.

Prezentace

Článek ve sborníku