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
Organization
keeletehnoloogia
Abstract
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.
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.
Graduation Theses defence year
2018-2019
Supervisor
Erkki Luuk
Spoken language (s)
Estonian, English
Requirements for candidates
Level
Bachelor, Masters
Application of contact
Name
Erkki Luuk
Phone
E-mail