■ ip), {
)
1 0 0 1
Tabulka 1.2: Tabulka pro spojku V (disjunkce)
v(cp) v{\p)
0 0 0
0 1 1
1 0 1
1 1 1
Tabulka 1.3: Tabulka pro spojku A (konjunkce)
v{ {1,0}, kde F je množina všech formulí výrokové logiky. Valuace výrokových proměnných jsou dány z vnějšku a valuace složených výroků je dána tabulkami 1.1,1.2, 1.3,1.4 a 1.5.
1.2 Predikátová logika
Predikátovou logiku lze chápat jako rozšíření logiky výrokové, která kromě pravdivostního ohodnocení výroků zkoumá vlastnosti objektů a vztahy mezi nimi.
Proměnné v ní nemají význam výroků, ale nahrazují objekty - individua, vlastnosti a vztahy mezi nimi jsou vyjádřeny pomocí predikátů. Kvantifikátory pak umožňují vyjádřit, že nějaká formule je platná pro všechna, nebo některá individua.
1.2.1 Syntaxe predikátové logiky
Jazyk predikátové logiky obsahuje:
• proměnné,
• funkční symboly (každý se svou četností neboli aritou),
• predikátové symboly (každý se svou četností neboli aritou),
• logické spojky (stejné jako ve výrokové logice),
• kvantifikátory (V - všeobecný, 3 - existenční).
25
i. Syntaxe a sémantika výrokové a predikátové logiky
Termy
Termy označují individua a jsou tvořeny konečnou posloupností aplikací následujících pravidel:
1. Každá proměnná je term.
2. Je-li / funkční symbol s aritou n a t\,tn jsou termy, je i/(ŕi,...,ŕ„) term.
Formule
Formule jsou tvrzení o individuích a jsou tvořeny konečnou posloupností aplikací následujících pravidel:
1. Je-li p predikátový symbol s aritou n a t\,tn jsou termy, je i p(h,tn) formule.
2. Jsou-li ý a xp formule, jsou i výrazy ->(p, (cp V xp), (cp A xp), ( ■ tp), { ■ F) psát (Vx G M)F, jako je to běžně zvykem. Analogickou syntaktickou zkratku zavedu pro existenční kvantifikátor 3.
Ze stejných důvodů zavedu i kvantifikátor jednoznačné existence (3!).
1.2.2 Sémantika predikátové logiky
Pro úvahy nad významem formulí je nutné specifikovat jeho interpretaci:
• množinu M, která obsahuje všechna individua,
• zobrazení f m typu Mn —> M pro každý funkční symbol /, kde n je jeho arita,
• relaci p m ^ MM pro každý predikátový symbol p, kde n je jeho arita.
Příkladem interpretace může být:
• M = Z.
• +, — nesou význam sčítání a odečítání celých čísel.
• <, = nesou význam „je menší než" a „rovná se".
Logické spojky pak nesou stejný význam jako ve výrokové logice.
27
2 Implementace syntaxí v jazyce Python
První částí elektronické přílohy práce - zdrojových kódů - je balíček logic, který obsahuje objektový model pro formule výrokové a predikátové logiky spolu se sadou předpřipravených funkčních a predikátových symbolů pro jejich snazší tvorbu.
Balíček jsem naprogramoval v jazyce Python [3], a to pouze s použitím jeho standardní knihovny, což znamená, že s sebou nenese další závislosti a bez instalace dalších nástrojů poběží všude, kde je k dispozici interpret jazyka Python ve verzi alespoň 3.9.
Tato kapitola obsahuje popis jednotlivých modulů a příklady jejich použití pro tvorbu formulí. Formule pak budou užitečné pro vytváření cvičení do webové aplikace (v kapitole 3).
2.1 Modul propositional
Modul propositional1 modeluje výrokovou logiku.
Modul obsahuje třídy Propositional Variable, Negation a LogicalConnective, které po řadě modelují výrokovou proměnnou, negaci formule a binární logickou spojku.
Pro tvůrce nebo tvůrkyni formulí jsou ale užitečnější pomocné funkce Variable, Conjunction, Disjunction, Implication a Equivalence, které umožňují jednoduchou tvorbu složitějších formulí, jak je vidět na příkladu.
Příklad2
from logic.propositional import (Variable, Conjunction, Disjunction, Implication)
X = VariableC'X") Y = VariableC'Y")
or_ = Disjunctions, Y) print(or_, or_.latex())
1. V elektronické příloze v souboru logic/propositional. py.
2. Také v elektronické příloze v souboru examples/propositional. py.
29
2. Implementace syntaxí v jazyce Python
and_ = Conjunction(X, Y) print(and_, and_.latex())
formula = Implication(and_, or_) print(formula, formula.latex())
Příklad po spuštění v Pythonu vypíše jak jednotlivé formule v prostém textu za použití matematických symbolů z tabulky Unicode, tak zdrojový kód pro sázecí program l^TgX.
Výstupem skriptu jsou tedy dle očekávání tyto tři formule:
• (XVY)
• (XAY)
• ((XAY) (XVY))
Funkce Variable přijímá jako argument jméno výrokové proměnné, funkce pro logické spojky pak dvě formule, které mají spojovat.
2.2 Modul predicate
Modul predicate3 modeluje predikátovou logiku.
Modul obsahuje třídy FunctionSymbol, PredicateSymbol, které modelují odpovídající syntaktické objekty predikátové logiky. Dále funkce Variable, ForAll a Exists pro tvorbu proměnných a kvantifikátorů.
Jejich použití ilustruji na příkladu níže, zdrojem formulí byly příklady v [4].
Příklad4
from logic.propositional import (Conjunction, Negation, Implication)
from logic.predicate import (Variable, ForAll, Exists, FunctionSymbol, PredicateSymbol)
3. V elektronické příloze v souboru logic/predicate. py.
4. Také v elektronické příloze v souboru examples/predicate. py.
30
2. Implementace syntaxí v jazyce Python
x = VariableCx")
S = PredicateSymbolCS", 1)
formula_l = Conjunction(
Exists(x, S(x)),
Exists(x, Negation(S(x))),
)
V = PredicateSymbol("V", 1)
formula_2 = ForAlKx, Implication(S(x), V(x)))
o = FunctionSymbol("o", 1) D = PredicateSymbolC'D", 1) H = PredicateSymbolC'H", 1)
formula_3 = Exists(x, Conjunction(D(x),H(o(x))))
print(formula_l, formula_l.latex()) print(formula_2, formula_2.latex()) print(formula_3, formula_3.latex())
Proměnné a logické spojky se používají stejně jako v případě výrokové logiky Funkční a predikátové symboly se instanciují určením jejich jména a parity a aplikují předáním termů do kulatých závorek.
l^TgXovým výstupem programu jsou tedy formule:
. (((3x)(S(x)))A((3x)((^S(x))))) . ((Vx)((S(x)^V(x)))) . ((3x)((D(x)AH(o(x)))))
2.3 Modul sets
Modul sets5 modeluje množiny, vztahy mezi nimi a jejich prvky.
Modul implementuje syntaxi množinové algebry: průnik a sjednocení pomocí funkcí Intersection a Union, stejně relaci incidence (In) a množinové relace (Superset a Subset).
Kromě toho obsahuje třídu SetsQuantif ier, která popisuje syntaktickou zkratku popsanou v 1.2.1 a pomocné funkce pro tvorbu kvantifikátorů s doménou: ForAll, Exists, Unique.
5. V elektronické příloze v souboru logic/sets. py
31
2. Implementace syntaxí v jazyce Python
Příklad6
from logic.sets import (ForAll, Variable, Set, In, Intersection, Union, Subset)
from logic.propositional import (Conjunction, Equivalence, Disjunction, Implication)
x = VariableC'x") A = SetC'A") B = SetC'B")
formula_l = Equivalence(
In(x, Intersections, B)),
Conjunction(In(x, A), In(x, B)),
)
formula_2 = Equivalence( In(x, Union(A, B)), Disjunction(In(x, A), In(x, B)),
)
formula_3 = Implication( Subset(A, B), ForAll(x, A, In(x, B)),
)
print(formula_l, formula_l.latex()) print(formula_2, formula_2.latex()) print(formula_3, formula_3.latex())
Výstupem skriptu jsou formule:
• ((x G (ADB)) ((x e A) A (x e B)))
• ((xe(AUB))&((xeA)v(xeB)))
• ((A CB)4 ((Vx G A)((x G B))))
6. Také v elektronické příloze v souboru examples/sets. py.
32
2. Implementace syntaxí v jazyce Python
2.4 Modul arithmetic
Modul arithmetic7 implementuje predikátové a funkční symboly pro operace (sčítání, odčítání,...) a relace (dělitelnost, uspořádání,...) nad čísly.
Jejich implementace jsou dobrými příklady toho, jak je možné balíček rozšířit o vlastní pomocné funkce.
7. V elektronické příloze v souboru logic/arithmetic. py.
33
3 Webová aplikace a tvorba cvičení
V této kapitole popíši dva typy cvičení pro převod matematických vyjádření z a do symbolického jazyka matematiky, proces jejich tvorby, organizace do sad a to, jak jsou prezentována studentům a studentkám ve webové aplikaci k řešení.
Každé cvičení se skládá z formule vytvořené za použití balíčku logic tak, jak je popsáno v kapitole 2, jejího ekvivalentu v jazyce přirozeném a volitelně dalších informací pro studenta nebo studentku a webovou aplikaci.
Cvičení vytvořená v jazyce Python jsou pak exportována do souboru ve formátu JSON [5], který je pak webovou aplikací interpretován do vizuální podoby v prostředí Blockly.
3.1 Prostředí Blockly
Webová aplikace používá open-source knihovnu Blockly [6] vyvíjenou společností Google. Ta se používá pro tvorbu blokových programů a vizuální programování. Bloky jsou grafické prvky, které běžně reprezentují různé programové konstrukce, jako jsou podmínky, smyčky a funkce. Uživatelky a uživatelé mohou bloky spojovat dohromady a tvořit tak programy bez nutnosti psát kód ručně.
Bloky v případě mojí aplikace reprezentují jednotlivé syntaktické objekty, ze kterých lze sestavit formule. Jsou generovány automaticky z definice formule nebo z jejího označkovaného popisu v přirozeném jazyce.
Mezi aplikace používající Blockly patří například Scratch [7] nebo Umíme informatiku [8]. Lze tedy očekávat, že se s prostředím Blockly někteří studenti a některé studentky přicházející na vysokou školu setkali už na škole střední nebo základní.
3.2 Převod z přirozeného do symbolického jazyka
V prvním typu cvičení je úkolem studentky nebo studenta na základě zápisu formule v přirozeném jazyce a významů predikátových
35
3- Webová aplikace a tvorba cvičení
Pokud bude pršet, zůstanu uvnitř.
• P ... bude pršet
• Q ... zůstanu uvnitř
t n i
Obrázek 3.1: Zadání cvičení pro převod ze symbolického zápisu.
a funkčních symbolů sestavit formuli z bloků odpovídající syntaktickým prvkům jazyka symbolického.
Příklad
Zdrojový kód níže obsahuje definici cvičení v jazyce Python a balíčku logic:
from logic.propositional import (Implication, Variable)
P = VariableC'P") Q = VariableC'Q")
cvičeni = (
Implication(P, Q),
"Pokud bude pršet, zůstanu uvnitř.", [
"P ... bude pršet",
"Q ... zůstanu uvnitř",
],
)
36
3- Webová aplikace a tvorba cvičení
Pokud bude pršet, zůstanu uvnitř.
• P ... bude pršet
• Q ... zůstanu uvnitř
Obrázek 3.2: Průběh řešení cvičení pro převod ze symbolického zápisu.
Pokud bude pršet, zůstanu uvnitř.
• P ... bude pršet
• Q ... zůstanu uvnitř
Obrázek 3.3: Vyřešené cvičení pro převod ze symbolického zápisu.
37
3- Webová aplikace a tvorba cvičení
(x e (A n B)) => (x e (A u B))
symetrického rozdílu
Patří-li lf x do množín A a B, patří i do jejich ftf
Obrázek 3.4: Zadání cvičení pro převod z přirozeného jazyka.
Definice cvičení je tedy trojice, která obsahuje formuli, řetězec s jejím překladem do přirozeného jazyka a seznam řetězců vysvětlujících významy jednotlivých symbolů použitých ve formuli.
Na obrázku 3.1 je výše definované cvičení v prostředí webové aplikace. Stavební kameny formule, výrokové proměnné P a Q a logická spojka =>, jsou umístěny v levém panelu a student nebo studentka je může volně přetahovat myší (nebo po dotykovém displeji) do volného prostoru v pravé části.
Snímek obrazovky 3.2 obsahuje stav z průběhu řešení. Pokud je cvičení vyřešeno správně, plocha s bloky se zbarví do zelena, jak je vidět na snímku obrazovky 3.3.
3.3 Převod ze symbolického do přirozeného jazyka
Druhým typem cvičení je převod ze symbolického zápisu do jazyka přirozeného. Úkolem studenta nebo studentky je v tomto případě doplnit do předpřipraveného bloku správná slova podle symbolického zápisu a volitelně podle významu jednotlivých symbolů.
Tvůrce nebo tvůrkyně příkladu v zadání označí pomocí hranatých závorek, která slova mají být v předpřipraveném bloku vynechána. Ta jsou pak spolu s distraktory umístěna v náhodném pořadí v levém panelu.
38
3- Webová aplikace a tvorba cvičení
(x e (A íl B)) => (x e (A U B))
Obrázek 3.5: Vyřešené cvičení pro převod z přirozeného jazyka. Příklad
Zdrojový kód níže obsahuje definici cvičení v jazyce Python a balíčku logic:
from logic.propositional import Implication from logic.predicate import ForAll cvičeni = (
ForAll(x, Implication(Ch(x), A(x))),
"[Každý], kdo [je chytrý], [dostane A]",
[
"Ch(x) ... x je chytrý", "A(x) ... x dostane A",
], [
"Žádný", "Neni chytrý",
],
)
Definice cvičení je tedy čtveřice, která obsahuje formuli, řetězec s jejím překladem do přirozeného jazyka s vyznačenými slovy k vynechání, seznam řetězců vysvětlujících významy jednotlivých symbolů
39
3- Webová aplikace a tvorba cvičení
použitých ve formuli a seznam distraktorů - řetězců, které budou přidány do levého panelu. Po správném sestavení bloků se plocha opět zbarví do zelena.
3.4 Tvorba sad
Sada je soubor v jazyce Python, který definuje skupinu cvičení na stejné téma. Příklady sad jsou v elektronické příloze ve složce exercises. Zde je příklad ze souboru exercises/sets . py.
from logic.sets import (Variable, Set, In, Intersection, Union)
from logic.propositional import (Conjunction, Equivalence, Implication)
NAME = "Množiny"
x = VariableC'x") A = Set("A") B = Set("B")
SYMBOLIC_ITEMS = [
(
Equivalence(
In(x, Intersections, B)), Conjunction(In(x, A), In(x, B)),
),
"x patři do průniku A a B právě tehdy, když x patři do A i do B.",
),
]
NATURAL_ITEMS = [
(
Implication(
In(x, Intersection^, B)), In(x, Union(A, B)),
),
"Patři-li [prvek] x do [průniku] množin A a B,\ patři i do jejich [sjednoceni]",
40
3- Webová aplikace a tvorba cvičení
[], [
"množina",
"symetrického rozdilu", "doplňku",
]
),
]
Sada musí obsahovat definici řetězce NAME, který obsahuje název dané sady, který se zobrazí jako tlačítko v záhlaví aplikace, a dva seznamy: SYMBOLIC_ITEMS, který obsahuje definice cvičení převodu do symbolického zápisu a NATURAL_ITEMS, který obsahuje definice cvičení pro převod opačným směrem.
Pomocí tlačítek v záhlaví aplikace lze přepínat mezi zobrazením všech cvičení pod sebou nebo jen konkrétní sady
3.5 Spuštění aplikace
Balíček logic je naprogramován v Pythonu bez dalších závislostí, webová aplikace je naprogramována v jazyce TypeScript s použitím knihovny Blockly. Před spuštění aplikace je nutné mít nainstalován interpret jazyka Python a balíčkovací systém NPM [9] pro instalaci závislostí webové aplikace.
V operačním systému Linux lze celou aplikaci spustit pomocí shellového skriptu runlocally.sh v kořenové složce elektronické přílohy. Podobné kroky lze však provést manuálně i na ostatních operačních systémech.
Skript nejprve spustí pythonový modul exercises/collect .py (příkaz python3 -m exercises. collect), který projde všechny soubory v této složce a posbírá z nich sady cvičení. Všechna cvičení pak exportuje do souboru web/src/exercises . j son. Dále spustí balíčkovací systém npm, který nainstaluje všechny potřebné knihovny pro spuštění webové aplikace a nakonec výslednou aplikaci spustí ve webovém prohlížeči.
Pro export aplikace pro nasazení na webovém hostingu lze použít skript deploy. sh. Ten celou aplikaci exportuje do složky web/dist,
41
3. Webová aplikace a tvorba cvičení
odkud ji lze nahrát na libovolný webový hosting. Aplikace je nasazena na webové adrese https : //bp. balazik. cz.
42
Závěr
Cílem této práce bylo vytvořit prototyp webové aplikace pro procvičování převodu symbolického zápisu matematických vyjádření z přirozeného jazyka a do něj.
V první kapitole jsem shrnul pojmy syntaxe výrokové a predikátové logiky a objasnil pravidla pro tvorbu jejich formulí.
Druhá kapitola popisuje implementaci balíčku logic v programovacím jazyce Python, který jsem pro potřeby této práce vytvořil. Ten slouží pro strukturovanou reprezentaci obecných logických formulí nad výrokovou a predikátovou logikou a poskytuje prostředky pro jejich tvorbu.
Ve třetí kapitole jsem popsal samotnou webovou aplikaci, která je naprogramovaná za použití open-source knihovny Blockly, která je de facto standardním nástrojem pro blokové programování. Implementoval jsem dva typy cvičení: jeden pro převod ze symbolického jazyka do jazyka přirozeného a druhý pro převod opačný.
Aplikace obsahuje několik cvičení, která slouží jako důkaz konceptu a nemají ambici být ucelenou sbírkou. Přikládám ale návod, jak do aplikace přidat nové sady cvičení a jak ji připravit pro nasazení na webovém serveru. Za přínosnou považuji nejen aplikaci samotnou, ale také balíček logic, který je připraven pro snadné rozšíření o další funkce pro reprezentaci formulí dalších odvětví matematiky.
Webová aplikace je nasazena na adrese https: //bp. balazik. cz. Všechny zdrojové kódy jsou uloženy v Archivu závěrečné práce v Informačním systému jako elektronická příloha.
43
Bibliografie
1. GLOSOVÁ, Pavla. Výuka formálního jazyka matematiky pomocí odpovědníků [online] [online]. 2019. [cit. 2023-05-08]. Dostupné z: https : //is .muni. cz/th/mklma/. SUPERVISOR : Ondřej Klíma.
2. PILÁT, Martin. Lecture Notes on Propositional and Predicate Logic [online]. 2023. [cit. 2023-05-09]. Dostupné z: https : //github . com/martinpilat/logic-book.
3. FOUNDATION, Python Software. Python [online]. 2023. [cit. 2023-05-08]. Dostupné z: https : //www. python. org/.
4. DEMLOVÁ, Marie. Příklady k předmětu DML [online]. 2005. [cit. 2023-05-09]. Dostupné z: https://kix.fsv.cvut.cz/~vanicek/ vyuka_109/demlova.pdf.
5. CROCKFORD, Douglas. The application/json Media Type for JavaScript Object Notation (JSON) [online]. 2006-07. [cit. 2023-05-09]. Request for Comments, RFC 4627. Internet Engineering Task Force. Dostupné z: https: //datatracker. ietf . org/doc/rf c4627/.
6. Blockly [online]. [B.r.]. [cit. 2023-05-09]. Dostupné z: https : // developers.google.com/blockly.
7. Blockly - Scratch Wiki [online]. [B.r.]. [cit. 2023-05-09]. Dostupné z: https://www.en.scratch-wiki.info/wiki/Blockly.
8. Umíme informatiku [online]. [B.r.]. [cit. 2023-05-09]. Dostupné z: https://www.umimeinformatiku.cz/.
9. npm [online]. [B.r.]. [cit. 2023-05-09]. Dostupné z: https : //www. npmjs.com/.
45
A Příloha
Elektronická příloha source. zip v Archivu práce v Informačním systému obsahuje všechny zdrojové kódy zmíněné v této práci.
A.1 Struktura elektronické přílohy
• Složka logic obsahuje zdrojové kódy balíčku v jazyce Python, který implementuje syntaxe výrokové a predikátové logiky.
• Složka exercises obsahuje soubory, ze kterých se generují sady cvičení pro webovou aplikaci.
• Složka examples obsahuje příklady zdrojových kódů použité v textu práce pro snazší kopírování.
• Složka text obsahuje jednotlivé části textu této práce ve značkovacím jazyce Markdown.
• Složka web obsahuje zdrojové kódy pro webovou aplikaci v jazycích HTML a TypeScript.
• Soubory run_locally. sh a deploy. sh jsou shellové skripty pro lokální spuštění a nasazení webové aplikace.
47