Город: Санкт-Петербург Новосибирск Казань Язык: Русский English

Interactive theorem proving and proof-checking
Автоматическое доказательство теорем

Что: Лекция
Когда: Воскресенье, 29 сентября 2013, 13:00–14:35
Где: ПОМИ РАН

Описание

Given that many problems in automated reasoning are undecidable or at least not feasible in practice, there has always been a strong interest in proof assistants that can help humans to construct formal proofs. I will talk about the architecture of such systems, with particular emphasis on the LCF approach.

Видео