Категория : Логика в информатике

Викискладе есть медиафайлы по теме логики в информатике .

Логика в информатике (или вычислительная логика ) — это раздел математической логики , который является примерно пересечением математической логики и информатики . Он содержит:

1. Те исследования в области логики, которые руководствуются приложениями в информатике . Например:
   • переписывания Системы , Комбинаторная логика и Абстрактная интерпретация ;
2. Фундаментальные концепции информатики, которые естественным образом выражаются в логической форме. Например:
   • Теория типов (используется в системах типов ), Формальная семантика языков программирования , Логика Хоара и Логическое программирование ;
3. Приложения фундаментальных концепций, заимствованных из теории вычислений , которые проливают свет на вопросы чистой логики. Например:
   • Переписка Карри-Ховарда и семантика игры ;
4. Инструменты для логиков, рассматриваемые как прикладная информатика . Например:
   • Автоматизированное доказательство теорем и проверка моделей .