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