Matej Petković: Agda v obliki za strojne učenjake

Agda je programski jezik z odvisnimi tipi, ki se ga lahko uporablja tudi za pomoč pri dokazovanju izrekov. Izrek v Agdi napišemo tako, da izjavo zapišemo kot tip, dokaz pa kot izraz tega tipa.

Med podajanjem izraza želenega tipa bi radi uporabili že prej dokazane leme (pomožne izreke), vendar se morda ne spomnimo njihovih imen ali pa ne vemo, katero lemo bi sploh lahko uporabili. Zato želimo ustvariti sistem za priporočanje, ki bi glede na tip in delno podan izraz uporabniku predlagal primerne leme.

Na seminarju bomo spoznali, kako so bile nekatere Agdine knjižnice pretvorjene v obliko, ki je primerna za strojno učenje (s-izrazi), kako so bili s-izrazi pretvorjeni v graf znanja, za zaključek pa si bomo ogledali še prve rezultate uporabe preprostih medot strojnega učenja.