NonClassicalLogics — различия между версиями

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
(Примерный список тем)
 
(не показано 60 промежуточных версии 2 участников)
Строка 1: Строка 1:
 +
Приветствуем Вас на странице факультатива "Неклассические логики", который читается на факультете компьютерных наук, начиная с 2020 года.
  
 
== О курсе ==
 
== О курсе ==
 
Курс знакомит с многообразием существующих логических систем. Основное внимание будет уделяться "нестандартным" логикам, тому, как логический способ мышления применяется к решению задач лингвистики, философии и информатики. Курс направлен на студентов ФКН академических программ бакалавриата “Программная инженерия” и “Прикладная математика и информатика”, но может быть интересен и студентам других программ, интересующихся логикой.
 
Курс знакомит с многообразием существующих логических систем. Основное внимание будет уделяться "нестандартным" логикам, тому, как логический способ мышления применяется к решению задач лингвистики, философии и информатики. Курс направлен на студентов ФКН академических программ бакалавриата “Программная инженерия” и “Прикладная математика и информатика”, но может быть интересен и студентам других программ, интересующихся логикой.
 +
 +
[https://cs.hse.ru/electives/nonclassical Официальная страница факультатива на сайте ФКН]
  
 
== Примерный список тем ==
 
== Примерный список тем ==
1. Понятие логики. Логика vs риторика. Формальный язык. Семантика. Система вывода. Непротиворечивость. Полнота. На примере исчисления высказываний.<br />
+
1. Понятие логики. Логика vs риторика. Формальный язык (на примере исчисления высказываний). Семантика. Система вывода. Корректность. Полнота. Дополнительно: пресуппозиция и импликатура. Постулаты Грайса. Перформативы. [http://newstar.rinet.ru/~goga/hse/non-classical-logics-2022/lecture1.pdf Слайды]<br />
2. Исчисление предикатов. Типизированное исчисление предикатов. Формальная семантика естественного языка.<br />
+
2. Исчисление предикатов. Арифметика Пеано. Теория множеств. [http://starlingdb.org/~goga/hse/non-classical-logics-2022/lecture2.pdf Слайды]<br />
3. Модальные логики. Модальность в естественном языке.<br />
+
3. Модальные логики. Логика контрафактивных условных предложений. Модальность в естественном языке. [http://starlingdb.org/~goga/hse/non-classical-logics-2022/lecture3.pdf Слайды]<br />
4. Интуиционизм. Темпоральные логики.  Динамическая логика.<br />
+
4. Интуиционизм. Темпоральная логика.  Динамическая логика. [http://starlingdb.org/~goga/hse/non-classical-logics-2022/lecture4.pdf Слайды]<br />
5. Логики, ориентированные на естественный язык. Логика контрафактивных условных предложений. Пресуппозиция и импликатура. Постулаты Грайса.<br />
+
5. Эпистемическая логика. Динамическая эпистемическая логика. Синтаксическая динамическая эпистемическая логика. Логика обоснования (justification logic). [http://starlingdb.org/~goga/hse/non-classical-logics-2022/lecture5.pdf Слайды]<br />
6. Эпистемическая логика. Динамическая эпистемическая логика. Синтаксическая динамическая эпистемическая логика. Логика доказательств.<br />
+
6. Логики, ориентированные на естественный язык. Формальная семантика. Обобщённые кванторы. Сдвиг типов. Продолжения. Динамическая логика предикатов. [http://starlingdb.org/~goga/hse/non-classical-logics-2022/lecture6.pdf Слайды]<br />
7. Субструктурные логики. Линейная логика. Категориальные грамматики.<br />
+
7. Субструктурные логики. Линейная логика. Категориальные грамматики. [http://starlingdb.org/~goga/hse/non-classical-logics-2022/lecture7.pdf Слайды]<br />
8. Логики, ориентированные на доказательство корректности компьютерных программ. Системы типов. Логика Хоара. Логика разделения (separation logic).<br />
+
8. Логики, ориентированные на доказательство корректности компьютерных программ. Системы типов. Логика Хоара. Сепарационная логика. [http://starlingdb.org/~goga/hse/non-classical-logics-2022/lecture8.pdf Слайды]<br />
 +
 
 +
== Список литературы ==
 +
 
 +
# '''Graham Priest. An Introduction to Non-Classical Logic. CUP, 2001. Главы 1-6.'''
 +
# Ernest Nagel, James R. Newman. Gödel's Proof. NYUP, 2001.
 +
# Kenneth Kunen. Set Theory. Elsevier, 1980. Глава 1.
 +
# Paul J. Cohen. Set Theory and the Continuum Hypothesis. NY: W.A. Benjamin, 1966.
 +
# '''Robert Goldblatt. Logics of Time and Computation. CSLI, 1992. Главы 1-10. [http://sul-derivatives.stanford.edu/derivative?CSNID=00003782&mediaType=application/pdf Ссылка]'''
 +
# С.П. Одинцов, С.О. Сперанский, С.А. Дробышевич. Введение в неклассические логики. РИЦ НГУ, 2014. [http://math.nsc.ru/~spodintsov/textbook.pdf Ссылка]
 +
# Angelika Kratzer. The Notional Category of Modality. 1981.
 +
# '''Hans van Ditmarsh, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic. Springer, 2008. Главы 1, 2, 4, 7.1-5.'''
 +
# Kurt Konolige. A Deduction Model of Belief. Pitman, 1986. Главы 1-2.
 +
# Sergei Artemov, Melvin Fitting. Justification Logic. Stanford Encyclopedia of Philosophy. [https://plato.stanford.edu/entries/logic-justification Ссылка]
 +
# Emmon Bach. Informal Lectures on Formal Semantics. SUNY Press, 1989.
 +
# Chris Barker, Chung-chieh Shan. Continuations and Natural Language. OUP, 2014.
 +
# Jeroen Groenendijk, Martin Stokhof. Dynamic Predicate Logic. In Linguistics and Philosophy 14(1):39-100 · 1991.
 +
# Emmanuel Beffara. Introduction to linear logic. Master. Italy. 2013. [https://hal.archives-ouvertes.fr/cel-01144229/document Ссылка]
 +
# Roberto Di Cosmo, Dale Miller. Linear Logic. Stanford Encyclopedia of Philosophy. [https://plato.stanford.edu/entries/logic-linear/ Ссылка]
 +
# Mark Steedman. The Syntactic Process. MIT Press, 2000. Главы 1-3.
 +
# Jason Baldridge. Lexically Specified Derivational Control in Combinatory Categorial Grammar. University of Edinburgh, 2002. Глава 2. [https://era.ed.ac.uk/bitstream/handle/1842/562/IP020026.pdf Ссылка]
 +
# Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Русский перевод: Бенджамин Пирс. Типы в языках программирования. Лямбда пресс, 2012.
 +
# Peter W. O'Hearn, Separation Logic. CACM, 2019. [https://cacm.acm.org/magazines/2019/2/234356-separation-logic/fulltext Ссылка]
 +
# Peter W. O'Hearn, Resources, Concurrency and Local Reasoning. Theoretical Computer Science, 2007. [http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf Ссылка]
  
 
== Расписание ==
 
== Расписание ==
=== Весна 2020 ===
+
=== Весна 2022 ===
Время занятий: 18:10 - 19:30 по четвергам<br />
+
Время занятий: 18:10 - 19:30 по понедельникам.<br />
 
Предварительный график:<br />
 
Предварительный график:<br />
30 января; 6, 13, 20, 27 февраля; 5, 12, 19 марта.
+
7, 14, 21, 28 февраля; 7, 14, 21, 28 марта.<br />
  
 
== Оценка ==
 
== Оценка ==
В качестве итоговой оценки за курс выставляется оценка, полученная на экзамене.<br />
+
Итоговая_оценка_за_курс = 0.5*оценка_за_работу_на курсе + 0.5*оценка_за_экзамен_либо_реферат.<br />
 +
Это актуальная формула!<br />
 +
 
 +
В ходе курса студентам будет предложено одно или несколько заданий по теме курса.
 +
Нужно будет разобраться в новом для себя материале, а также подготовить эссе, основанное на материалах исследовательских работ. <br />
 
Шкала оценки - десятибалльная. Округление - стандартное арифметическое.
 
Шкала оценки - десятибалльная. Округление - стандартное арифметическое.
 +
 +
=== Возможные темы для рефератов или эссе ===
 +
 +
# Повышающая теорема Лёвенгейма-Сколема (исправить доказательство из лекции).
 +
# Логика GL. Отсутствие компактности, слабая полнота.
 +
# Временные логики ''LinDist'', ''LinRat'', ''LinRe'' (По Goldblatt 1992, глава 8, любая одна на выбор). Доказательство полноты относительно соответствующего класса шкал.
 +
# Динамическая логика высказываний либо эпистемическая логика S5C. Доказательство слабой полноты.
 +
# Линейная логика. Устранение сечения.
 +
# Исчисление Ламбека. Схема доказательства эквивалентности контекстно-свободным грамматикам.
  
 
== Автор и лектор курса ==
 
== Автор и лектор курса ==
Георгий Бронников, разработчик компании JetBrains.
+
'''Георгий Бронников''' - программист, лингвист. yura.bronnikov собака gmail.com
  
 
== Благодарности ==
 
== Благодарности ==
 
Факультатив проходит при поддержке компании [https://jetbrains.ru/ JetBrains].
 
Факультатив проходит при поддержке компании [https://jetbrains.ru/ JetBrains].

Текущая версия на 04:13, 2 апреля 2022

Приветствуем Вас на странице факультатива "Неклассические логики", который читается на факультете компьютерных наук, начиная с 2020 года.

О курсе

Курс знакомит с многообразием существующих логических систем. Основное внимание будет уделяться "нестандартным" логикам, тому, как логический способ мышления применяется к решению задач лингвистики, философии и информатики. Курс направлен на студентов ФКН академических программ бакалавриата “Программная инженерия” и “Прикладная математика и информатика”, но может быть интересен и студентам других программ, интересующихся логикой.

Официальная страница факультатива на сайте ФКН

Примерный список тем

1. Понятие логики. Логика vs риторика. Формальный язык (на примере исчисления высказываний). Семантика. Система вывода. Корректность. Полнота. Дополнительно: пресуппозиция и импликатура. Постулаты Грайса. Перформативы. Слайды
2. Исчисление предикатов. Арифметика Пеано. Теория множеств. Слайды
3. Модальные логики. Логика контрафактивных условных предложений. Модальность в естественном языке. Слайды
4. Интуиционизм. Темпоральная логика. Динамическая логика. Слайды
5. Эпистемическая логика. Динамическая эпистемическая логика. Синтаксическая динамическая эпистемическая логика. Логика обоснования (justification logic). Слайды
6. Логики, ориентированные на естественный язык. Формальная семантика. Обобщённые кванторы. Сдвиг типов. Продолжения. Динамическая логика предикатов. Слайды
7. Субструктурные логики. Линейная логика. Категориальные грамматики. Слайды
8. Логики, ориентированные на доказательство корректности компьютерных программ. Системы типов. Логика Хоара. Сепарационная логика. Слайды

Список литературы

  1. Graham Priest. An Introduction to Non-Classical Logic. CUP, 2001. Главы 1-6.
  2. Ernest Nagel, James R. Newman. Gödel's Proof. NYUP, 2001.
  3. Kenneth Kunen. Set Theory. Elsevier, 1980. Глава 1.
  4. Paul J. Cohen. Set Theory and the Continuum Hypothesis. NY: W.A. Benjamin, 1966.
  5. Robert Goldblatt. Logics of Time and Computation. CSLI, 1992. Главы 1-10. Ссылка
  6. С.П. Одинцов, С.О. Сперанский, С.А. Дробышевич. Введение в неклассические логики. РИЦ НГУ, 2014. Ссылка
  7. Angelika Kratzer. The Notional Category of Modality. 1981.
  8. Hans van Ditmarsh, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic. Springer, 2008. Главы 1, 2, 4, 7.1-5.
  9. Kurt Konolige. A Deduction Model of Belief. Pitman, 1986. Главы 1-2.
  10. Sergei Artemov, Melvin Fitting. Justification Logic. Stanford Encyclopedia of Philosophy. Ссылка
  11. Emmon Bach. Informal Lectures on Formal Semantics. SUNY Press, 1989.
  12. Chris Barker, Chung-chieh Shan. Continuations and Natural Language. OUP, 2014.
  13. Jeroen Groenendijk, Martin Stokhof. Dynamic Predicate Logic. In Linguistics and Philosophy 14(1):39-100 · 1991.
  14. Emmanuel Beffara. Introduction to linear logic. Master. Italy. 2013. Ссылка
  15. Roberto Di Cosmo, Dale Miller. Linear Logic. Stanford Encyclopedia of Philosophy. Ссылка
  16. Mark Steedman. The Syntactic Process. MIT Press, 2000. Главы 1-3.
  17. Jason Baldridge. Lexically Specified Derivational Control in Combinatory Categorial Grammar. University of Edinburgh, 2002. Глава 2. Ссылка
  18. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Русский перевод: Бенджамин Пирс. Типы в языках программирования. Лямбда пресс, 2012.
  19. Peter W. O'Hearn, Separation Logic. CACM, 2019. Ссылка
  20. Peter W. O'Hearn, Resources, Concurrency and Local Reasoning. Theoretical Computer Science, 2007. Ссылка

Расписание

Весна 2022

Время занятий: 18:10 - 19:30 по понедельникам.
Предварительный график:
7, 14, 21, 28 февраля; 7, 14, 21, 28 марта.

Оценка

Итоговая_оценка_за_курс = 0.5*оценка_за_работу_на курсе + 0.5*оценка_за_экзамен_либо_реферат.
Это актуальная формула!

В ходе курса студентам будет предложено одно или несколько заданий по теме курса. Нужно будет разобраться в новом для себя материале, а также подготовить эссе, основанное на материалах исследовательских работ.
Шкала оценки - десятибалльная. Округление - стандартное арифметическое.

Возможные темы для рефератов или эссе

  1. Повышающая теорема Лёвенгейма-Сколема (исправить доказательство из лекции).
  2. Логика GL. Отсутствие компактности, слабая полнота.
  3. Временные логики LinDist, LinRat, LinRe (По Goldblatt 1992, глава 8, любая одна на выбор). Доказательство полноты относительно соответствующего класса шкал.
  4. Динамическая логика высказываний либо эпистемическая логика S5C. Доказательство слабой полноты.
  5. Линейная логика. Устранение сечения.
  6. Исчисление Ламбека. Схема доказательства эквивалентности контекстно-свободным грамматикам.

Автор и лектор курса

Георгий Бронников - программист, лингвист. yura.bronnikov собака gmail.com

Благодарности

Факультатив проходит при поддержке компании JetBrains.