arvutiteaduse instituudi lõputööde teemade register


Tavakeele morfoloogia, süntaksi, semantika ja/või pragmaatika tüübiteoreetiline formaliseerimine ja teoreemitõestus | Type-theoretical formalization and theorem proving in natural language morphology, syntax, semantics and/or pragmatics
Organisatsiooni nimikeeletehnoloogia
KokkuvõteTavakeele morfoloogia, süntaksi, semantika ja/või pragmaatika tüübiteoreetiline formaliseerimine ja teoreemitõestus (BSc/MSc)

Tegu on valdkonnaga, mis sisaldab kaht (omavahel kombineeritavat) teemadehulka: 1. Tõestusprogrammide (Agda, Coq, Lean...) kasutamine tavakeele morfoloogia, süntaksi, semantika ja/või pragmaatika fragmentide formaliseerimisel, vb ka formaliseeringut puudutavate teoreemide tõestamisel või olemasolevate tavakeele kohta käivate "teoreemide" ümberlükkamisel. 2. Grammatical Framework'i (GF) kasutamine tavakeele morfoloogia, süntaksi, semantika ja/või pragmaatika fragmentide formaliseerimisel. Formaliseeritav fragment võib kirjeldada mistahes konkreetset tavakeelt või olla keelteülene (universaalne). Sõltuvalt teemast oleks siin ainest nii baka- kui ka magistritööks. Vajalik on piisav huvi valdkonna vastu, et võimalikku teemat selle piires *esialgsel* kujul ise defineerida (juhendaja saab selle täpsustamisel aidata). Soovitav on eelnev kokkupuude tõestusprogrammidega, tavakeele uurimisega või GFga. Sõltuvalt teemast võib osutuda vajalikuks kaasjuhendamine. Teema lõplik defineerimine eeldab kokkulepet juhendaja(te)ga. Lisainfo:

https://coq.inria.fr/
http://wiki.portal.chalmers.se/agda/pmwiki.php
https://leanprover.github.io/
http://www.grammaticalframework.org/

---------------

Type-theoretical formalization and theorem proving in natural language morphology, syntax, semantics and/or pragmatics (Bsc/Msc)

This field comprises two (combinable) sets of topics: 1. Using proof assistants (Agda, Coq, Lean...) in formalizing natural language (NL) morphology, syntax, semantics and/or pragmatics, possibly proving theorems about the formalization or disproving exsisting "theorems" about NL. 2. Using Grammatical Framework (GF) to formalize fragments of NL morphology, syntax, semantics and/or pragmatics. The fragment to be formalized may be language-particular or universal. Depending on the topic, this could be a Bachelor or Masters thesis. Choosing a topic from this field presumes sufficient interest in the field to specify a *preliminary* topic (the supervisor can help in specifying it). Prior acquaintance with proof assistants, GF or research on natural language is desirable. Depending on the topic, co-supervision may be necessary. The final specification of the topic presumes supervisor(s') consent. More information is available on the links above.
Lõputöö kaitsmise aasta2018-2019
JuhendajaErkki Luuk
Suhtlemiskeel(ed)eesti keel, inglise keel
Nõuded kandideerijale
Tase Bakalaureus, Magister
Märksõnad #type_theory #tüübiteooria #tavakeel #natural_language
Kandideerimise kontakt
Nimi Erkki Luuk
Tel
E-mail erkkil@gmail.com


ati.study@lists.ut.ee