Автоматическое доказательство теорем

Общая информация
ЛекторДж. Харрисон
Семестросень 2013
Дата начала28.09.2013
Количество пар5
Язык курсаанглийский
Аннотация In these lectures I will give a general overview of automated theorem proving in the broad sense, including fully automated methods, interactive methods and their applications in both mathematics and computing. The content of the course will be quite strongly influenced by my book http://www.cambridge.org/9780521899574 and its associated code, but will be more high-level and include more discussion of applications.
Слайды первой лекции
from
Лекции Подсказка: слайды, видеозапись и другие материалы лекции доступны со страницы лекции, попасть на которую можно, нажав на её название.

1. Background, history and propositional logic
(28.09.2013 - 17:20 - 18:55)

I will describe some of the highlights of the history of how automated theorem proving developed, and some of the main areas of interest. I will then precisely define some foundational material and talk about decision methods for propositional logic (SAT). http://www.youtube.com/watch?v=Nydg-N83VYc
2. First-order logic with and without equality
(28.09.2013 - 19:05 - 20:40)

Here I will discuss first-order logic and the various methods for its semi-automation (tableaux, inverse method, resolution, model elimination), as well as some methods for equational reasoning. This was one of the primary interests in the 1970s and it still an active field today. http://www.youtube.com/watch?v=iPFJY0aW4E4
3. Decidable problems in logic and algebra
(29.09.2013 - 11:15 - 12:50)

There are many non-trivial problems of logic that are, at least in principle, decidable. I will discuss some of these, emphasizing decision procedures in interesting theories that often generalize traditional mathematical methods (quantifier elimination, Groebner bases, SMT solvers). http://www.youtube.com/watch?v=ZdJ0-V77f_0
4. Interactive theorem proving and proof-checking
(29.09.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". http://www.youtube.com/watch?v=g3EQKBMq5h0
5. Applications to mathematics and computer verification
(29.09.2013 - 15:35 - 17:10)

As well as general intellectual interest and the study of artificial intelligence, automated theorem proving has been applied both to problems in pure mathematics and computer system verification, and I'll describe some interesting instances.
Ваша оценка: Пусто Средняя: 4.6 (9 votes)
Share |