×
Универзитет у Новом Саду

Предмет: Интерактивни доказивачи (17.DOM71)

Основне информације:
 
Категорија Научно-стручни
Ужа научна област
  • Примењене рачунарске науке и информатика
  • Теоријска и примењена математика
ЕСПБ 10

Стицање знања и практичан рад са интерактивним доказивачима COQ, ISABELL/HOL. Укључивање студента у научно-истраживачки рад.

Познавање теоријских основа и практичног рада са интерактивним доказивачима теорема. Укључивање у актуелна истраживања у домену интерактивних доказивача, по избору студента, а у сарадњи са научницима из земље и иностранства.

Теоретске основе интерактивних доказивача. Уводни појмови из теорије типова: типови, терми. Разни типски системи. Типски систем са основним (простим) типом. Основне дефиницје и особине. Конфлуентност и теореме о нормализацијама доказа. Полиморфни типски систем. Теорема о јакој нормализацији, њен доказ и значај као пример Геделове реченице. Типски системи са зависним типовима. Теорија конструкција (Coquand). Увод у основне појмове интерактивног доказивања теорема. Доказивачи теорема: COQ и ISABELLE.

На предавањима се излаже теоретски део градива пропраћен карактеристичним примерима ради лакшег разумевања градива. Студент самостално проучава додатну литературу и дискутује је са наставником на консултацијама.

Аутори Назив Година Издавач Језик
COQ Team The COQ Proof Assitant 2018 https://coq.inria.fr/ Енглески
Зоран Огњановић, Силвиа Гилезан Теоријско рачунарство 2018 Српски језик
Nipkow, T., Paulson, L., Wenzel, M. Isabelle/HOL : A Proof Assistant for Higher-Order Logic 2002 Springer, Berlin Енглески
Benjamin Pierce Software Foundations 2018 https://softwarefoundations.cis.upenn.edu/current/index.html Енглески
Предметна активност Предиспитна Обавезна Број поена
Предметна активност
Семинарски рад
Предиспитна
Да
Обавезна
Да
Број поена
50.00
Предметна активност
Усмени део испита
Предиспитна
Не
Обавезна
Да
Број поена
50.00
API Image

проф. др Силвиа Гилезан

Редовни професор

Предавања

API Image

проф. др Силвиа Гилезан

Редовни професор

Студијски истраживачки рад