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 nimi
keeletehnoloogia
Kokkuvõte
Tavakeele 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 aasta
2018-2019
Juhendaja
Erkki 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