City: Saint Petersburg Novosibirsk Kazan Language: Русский English

Interactive theorem proving and proof-checking
A survey of automated theorem proving

What: Lecture
When: Sunday, 29 September 2013, 13:00–14:35
Where: ПОМИ РАН

Description

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.

Video