Speaker / Predavač : Petar Maksimovic
Title / Naslov: General Logical Framework i formalizacija dela probabilisticke logike LPP2 u dokazivacu teorema Coq.
Abstract / Abstrakt:
U prvom delu ovog izlaganja bice predstavljen General Logical Framework, lambda-racun sa generalizovanom apstrakcijom, u kojem izvrsavanje beta-redukcije zavisi od toga da li argument zadovoljava dat logicki predikat, i bice prikazano kako se iz ovog racuna mogu dobiti neki poznati lambda-racuni. U drugom delu izlaganja bice predstavljena formalizacija sintakse i semantike probabilisticke logike LPP2 u Coq-u, kao i formalni dokaz teoreme saglasnosti za tu logiku.".