|
|
Rozpoznávání obrázkových jazyků
Barták, Jakub ; Mráz, František (vedoucí práce) ; Plátek, Martin (oponent)
Předkládáme zde transformaci jednodimenzionálního zkracujícího restartovacího automatu do dvou dimenzí. Výsledný automat (zvaný dvoudimenzionální restartovací automat - 2RA) má jak zajímavé uzávěrové vlastnosti, tak blízkou vazbu na třídu jazyků REC (Recognizable languages), čímž se třída jazyků které je schopen rozpoznat ukazuje být zajímavým přínosem pro hierarchii dvou-dimenzionálních jazyků.
|
|
|
Strojové učenie formálnych jazykov
Klonfar, Matěj ; Mráz, František (vedoucí práce) ; Plátek, Martin (oponent)
V předložené práci studuji úlohu strojového učení formálních jazyků. Úlohou práce je navrhnout a implementovat program umožňující studovat průběh a výsledky jednotlivých algoritmů na učení jazyků. Program podporuje učení z příkladů zadaných vstupní množinou pozitivních a negativních příkladů nebo učitelem, znajícím cílový jazyk. Program poskytuje nástroj na testování naučených jazyků. Hlavním cílem práce je navrhnout program s ohledem na snadné rozšiřování o další implementace algoritmů bez omezení na použité reprezentace naučených jazyků či složitosti těchto jazyků.
|
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (vedoucí práce) ; Haniková, Zuzana (oponent) ; Plátek, Martin (oponent)
In this thesis we deal with the problem of automatic proving (or disproving) mathematical conjectures using computer programs (usually called automated theorem provers). We address several issues that are important for a successful utilization of such programs. In Chapter 3 we examine how to store and reuse important pieces of mathematical knowledge in the form of lemmas. We investigate how this process can be automatized, i.e. how a computer can construct and use lemmas without human guidance. The program we develop tries to shorten or to speed up the proofs of several conjectures from a common theory. It repeatedly extracts lemmas from the proofs it has already completed and uses the lemmas to improve the sets of premisses to produce more efficient proofs of the conjectures. In Chapter 4 we develop a new algorithm that tries to construct the optimal sets of premisses for proving and disproving mathematical conjectures. The algorithm semantically analyzes the conjectures and the set of premisses of the given theory to find the optimal subsets of the premisses. The algorithm uses an automated model finder to construct models that serve as counterexamples that guide the algorithm to find the optimal set of premisses. In Chapter 5 we use the algorithm to decide formulae in a wide range of modal systems. We...
|
|
|
Generátor kompilátorů založený na restartovacích automatech
Procházka, Jan ; Mráz, František (vedoucí práce) ; Plátek, Martin (oponent)
Restartovací automaty jsou velmi silný teoretický model, který umožňuje (ve své nejobecnější variantě) rozpoznávat mnohem širší třídu jazyků, než je třída jazyků bezkontextových. Cílem této práce bylo vytvořit nástroj, který pro daný restartovací automat zapsaný pro člověka čitelnou formou generuje program počítající význam vstupního textu. Bylo proto nutné model rozšířit o sémantiku. Výsledný nástroj je generátor kompilátorů (CCRA) a vychází z nástrojů jako je flex, či bison, ale místo bezkontextové gramatiky používá restartovací automat. Je napsaný v jazyce C++ tak, aby bylo možné ho používat jak na systémech Windows, tak Linux. Stejný jazyk používá pro svůj výstup.
|
|
|
Strojové učenie formálnych jazykov
Klonfar, Matěj ; Mráz, František (vedoucí práce) ; Plátek, Martin (oponent)
V předložené práci studuji úlohu strojového učení formálních jazyků. Úlohou práce je navrhnout a implementovat program umožňující studovat průběh a výsledky jednotlivých algoritmů na učení jazyků. Program podporuje učení z příkladů zadaných vstupní množinou pozitivních a negativních příkladů nebo učitelem, znajícím cílový jazyk. Program poskytuje nástroj na testování naučených jazyků. Hlavním cílem práce je navrhnout program s ohledem na snadné rozšiřování o další implementace algoritmů bez omezení na použité reprezentace naučených jazyků či složitosti těchto jazyků.
|
|
|
Natural Language Processing of Textual Use Cases
Dražan, Jaroslav ; Mencl, Vladimír (vedoucí práce) ; Plátek, Martin (oponent)
Požadavky na funkčnost navrhovanému systému jsou obvykle zachycovány pomocí use case psaných v přirozeném jazyce. Formát use case není standardizován, nicméně věty use case mají tradični jednoduchou strukturu a popisují buď komunikaci mezi aktéry a navrhovaným systémem, nebo interní akce. Přirozený jazyk se používá, nebo je srozumitelný pro zainteresované strany a je dostatečný k zachycení většiny požadavků, bohužel ale díky jeho volnosti není možné snadno automatizovat jeho analyzování. Vladimír Mencl použil současné lingvistické nástroje, aby získal popis chování navrhovaného systému z use case napsaných v přirozeném jazyce. Specifikaci chování zachycuje ve formi pro-case. Z jeho práce vyplývá, že je to možné, ale také se objevilo několik problémů, které daná práce neřeší. A právě některé z těchto problémů řešíme v této diplomové práci. Popisujeme v ní algoritmus odvozený od původního Menclova algoritmu, který umožní zpracovat více typů use case než ten původní, a navrhujeme metriku, která měří kvalitu parse stromů. Tato metrika umožňuje výběr nejlepšího parse stromu use case věty z několika parse stromů vytvořených pomocí různých lingvistických parserů. To pomáhá eliminovat problémy s tím, že jeden parser vrátí chybný výstup.
|
|
|
Lexicalized Syntactic Analysis by Restarting Automata
Mráz, F. ; Otto, F. ; Pardubská, D. ; Plátek, Martin
We study h-lexicalized two-way restarting automata that can rewrite at most i times per cycle for some i ≥ 1 (hRLWW(i)-automata). This model is considered useful for the study of lexical (syntactic) disambiguation, which is a concept from linguistics. It is based on certain reduction patterns. We study lexical disambiguation through the formal notion of h-lexicalized syntactic analysis (hLSA). The hLSA is composed of a basic language and the corresponding h-proper language, which is obtained from the basic language by mapping all basic symbols to input symbols. We stress the sensitivity of hLSA by hRLWW(i)-automata to the size of their windows, the number of possible rewrites per cycle, and the degree of (non-)monotonicity. We introduce the concepts of contextually transparent languages (CTL) and contextually transparent lexicalized analyses based on very special reduction patterns, and we present two-dimensional hierarchies of their subclasses based on the size of windows and on the degree of synchronization. The bottoms of these hierarchies correspond to the context-free languages. CTL creates a proper subclass of context-sensitive languages with syntactically natural properties.
|
|
|
Hierarchické modelování plánovacích problémů
Dvořák, Tomáš ; Barták, Roman (vedoucí práce) ; Plátek, Martin (oponent)
Automatické plánování je problém nalezení sekvence akcí vedoucích z daného počátečního stavu do požadovaného cílového stavu. Existuje celá řada formálních modelů určených pro modelování plánovacích problémů. Jednou z větví je třída formálních modelů umožňujících definovat hierarchickou strukturu mezi akcemi. Tato práce navrhuje hierarchický model, nazvaný GramPlan, založený na atributových gramatikách. Ukazuje několik způsobů jak lze na GramPlan převést problém zadaný klasickým STRIPS formalismem a dokazuje korektnost těchto převodů. Práce předvádí převod workflow z FlowOpt formalismu na GramPlan a dokazuje korektnost takového převodu. Nakonec jsou navrhnuty dva způsoby jak GramPlan model verifikovat a je dokázáno, že jsou ekvivalentní a dávají stejný výsledek. Powered by TCPDF (www.tcpdf.org)
|
|
|
Redukční automaty a syntaktické chyby
Procházka, Martin ; Plátek, Martin (vedoucí práce) ; Pardubská, Dana (oponent) ; Průša, Daniel (oponent)
Tato práce se zabývá redukčními automaty, jejich normalizacemi a využitím pro (robustní) redukční analýzu a lokalizaci syntaktických chyb pro jazyky ze třídy DCFL. Redukční automat navazuje na restartovací automat, od kterého se odlišuje explicitním určením redukovaných symbolů (to umožňuje přesné určení místa chyby) a přesunem výhledového okna do stavu řídící jednotky (ten ho přibližuje zařízením studovaným klasickou teorií automatů a formálních jazyků). Pro redukční automat pak lze snadněji než pro automat restartovací přebírat pojmy a postupy klasické teorie, jako je např. prefixová korektnost nebo minimalizace množiny stavů. Pro libovolný neprázdný jazyk ze třídy DCFL zadaný monotónním redukčním automatem, navíc ještě prefixově korektním a stavově minimálním, navrhujeme metodu robustní redukční analýzy, která zaručuje lokalizaci formálně definovaných typů skutečných (nezavlečených) chyb, bezchybných podslov a míst redukčních konfliktů (podslov s nejednoznačnou syntaktickou strukturou redukovatelných v různých slovech různými způsoby). Navrhovanou metodu implementujeme novým typem zařízení (postprefixovým robustním analyzátorem) a stručně ukazujeme, jak jí implementovat deterministickým zásobníkovým převodníkem pracujícím v lineárním čase vzhledem k délce slova.
|
|
|
Strojové učenie formálnych jazykov
Klonfar, Matěj ; Mráz, František (vedoucí práce) ; Plátek, Martin (oponent)
V předložené práci studuji úlohu strojového učení formálních jazyků. Úlohou práce je navrhnout a implementovat program umožňující studovat průběh a výsledky jednotlivých algoritmů na učení jazyků. Program podporuje učení z příkladů zadaných vstupní množinou pozitivních a negativních příkladů nebo učitelem, znajícím cílový jazyk. Program poskytuje nástroj na testování naučených jazyků. Hlavním cílem práce je navrhnout program s ohledem na snadné rozšiřování o další implementace algoritmů bez omezení na použité reprezentace naučených jazyků či složitosti těchto jazyků.
|
host ::
RSS.