Логическая структура
-
Основы логической структуры
- Логическая структура позволяет представить логику в виде сигнатуры в теории типов.
- Доказательство формул в исходной логике сводится к определению типа в теории типов.
-
История и развитие
- Первым логическим фреймворком был Automath, но более известен эдинбургский логический фреймворк LF.
- Современные инструменты проверки, такие как Isabelle, основаны на этой идее.
-
Описание и особенности
- Логическая структура основана на зависимом лямбда-исчислении и имеет три уровня: объекты, типы и разновидности.
- Вывод типа в λΠ-исчислении неразрешим, но хорошо типизированные термины строго нормализуемы.
- Суждения представлены в виде типов их доказательств, что соответствует кантовскому понятию суждения.
-
Реализация и методология
- Система Twelf в Университете Карнеги-Меллона обеспечивает реализацию логической структуры LF.
- Система включает в себя механизм логического программирования и метатеоретические рассуждения.
-
Дополнительные ресурсы
- В статье приведены ссылки на другие работы и внешние ресурсы, связанные с логической структурой и реализацией.