Логическая структура

В логике логическая структура предоставляет средства для определения (или представления) логики как сигнатуры в теории типов более высокого порядка таким образом, что доказуемость формулы в исходной логике сводится к проблеме обитания типа в структуре type. теория. ^[1]^[2]Этот подход успешно использовался для (интерактивного) автоматического доказательства теорем . Первой логической структурой был Automath ; однако название идеи происходит от более широко известной Эдинбургской логической структуры, LF . Несколько более поздних инструментов доказательства, таких как Isabelle, основаны на этой идее. ^[1] В отличие от прямого внедрения, подход логической структуры позволяет встроить множество логик в систему одного и того же типа. ^[3]

Обзор [ править ]

Логическая структура основана на общей обработке синтаксиса, правил и доказательств посредством зависимо типизированного лямбда-исчисления . Синтаксис рассматривается в стиле, похожем на Пера Мартина-Лёфа систему аритетов , но более общий.

Для описания логической структуры необходимо предоставить следующее:

Характеристика класса представляемой объектной логики;
Соответствующий метаязык;
Характеристика механизма представления объектной логики.

Это резюмируется следующим образом:

« Структура = Язык + Представление ».

ЛФ [ править ]

В случае логической структуры LF метаязыком является λΠ-исчисление . Это система зависимых типов функций первого порядка, которые связаны принципом предложений как типов с первого порядка минимальной логикой . Ключевые особенности λΠ-исчисления состоят в том, что оно состоит из сущностей трех уровней: объектов, типов и видов (или классов типов, или семейств типов). Он предикативен , все хорошо типизированные термины строго нормализуют и Черча-Россера , а свойство хорошо типизированности разрешимо . Однако вывод типа неразрешим.

Логика представлена в логической структуре LF с помощью механизма представления суждений как типов. Это вдохновлено Пером Мартином-Лёфом развитием кантовского понятия суждения в Сиенских лекциях 1983 года. Два суждения высшего порядка, гипотетическое $J\vdash K$ и генерал, $\Lambda x\in J.K(x)$ , соответствуют обычному и зависимому функциональному пространству соответственно. Методология суждений-типов заключается в том, что суждения представляются как типы их доказательств. Логическая система ${\mathcal {L}}$ представлен своей сигнатурой, которая присваивает виды и типы конечному набору констант, представляющих его синтаксис, его суждения и схемы правил. Правила и доказательства объектной логики рассматриваются как примитивные доказательства гипотетико-общих суждений. $\Lambda x\in C.J(x)\vdash K$ .

Реализацию логической структуры LF обеспечивает система Twelf в Университете Карнеги-Меллон . Двенадцать включает в себя

механизм логического программирования
метатеоретические рассуждения о логических программах (завершение, покрытие и т. д.)
индуктивное металогическое средство доказательства теорем

См. также [ править ]

Ссылки [ править ]

^ Перейти обратно: ^а ^б Барт Джейкобс (2001). Категориальная логика и теория типов . Эльзевир. п. 598. ИСБН 978-0-444-50853-9 .
^ Дов М. Габбай, изд. (1994). Что такое логическая система? . Кларендон Пресс . п. 382. ИСБН 978-0-19-853859-2 .
^ Ана Бове; Луис Соареш Барбоза; Альберто Пардо (2009). Языковая инженерия и тщательная разработка программного обеспечения: Международная летняя школа LerNet ALFA 2008, Пириаполис, Уругвай, 24 февраля - 1 марта 2008 г., переработанная версия, избранные статьи . Спрингер. п. 48. ИСБН 978-3-642-03152-6 .

Дальнейшее чтение [ править ]

Фрэнк Пфеннинг (2002). «Логические структуры – краткое введение». В Хельмуте Швихтенберге , Ральфе Штайнбрюггене (ред.). Доказательство и надежность системы (PDF) . Спрингер . ISBN 978-1-4020-0608-1 .
Роберт Харпер , Фурио Хонселл и Гордон Плоткин . Структура для определения логики . Журнал Ассоциации вычислительной техники, 40(1):143-184, 1993.
Арнон Аврон , Фурио Хонселл, Ян Мейсон и Рэнди Поллак. Использование типизированного лямбда-исчисления для реализации формальных систем на машине . Журнал автоматического рассуждения, 9:309-354, 1992.
Роберт Харпер. Эквациональная формулировка LF . Технический отчет, Эдинбургский университет , 1988 г. Отчет LFCS ECS-LFCS-88-67.
Роберт Харпер, Дональд Саннелла и Анджей Тарлецкий. Презентации структурированной теории и логические представления . Анналы чистой и прикладной логики, 67 (1–3): 113–160, 1994.
Самин Иштиак и Дэвид Пим. Соответствующий анализ естественной дедукции . Журнал логики и вычислений 8, 809–838, 1998.
Самин Иштиак и Дэвид Пим. Ресурсные модели Крипке зависимо типизированного группированного $\lambda$ -исчисление . Журнал логики и вычислений 12 (6), 1061–1104, 2002.
Пер Мартин-Лёф. « О значении логических констант и обосновании логических законов ». « Северный журнал философской логики », 1 (1): 11-60, 1996.
Бенгт Нордстрем, Кент Петерссон и Ян М. Смит. Программирование в теории типов Мартина-Лёфа . Oxford University Press , 1990. (Книга больше не издается, но бесплатная версия .) доступна
Дэвид Пим. Замечание о теории доказательств $\lambda \Pi$ -исчисление . Студия Логика 54: 199–230, 1995.
Дэвид Пим и Линкольн Уоллен . Поиск доказательств в $\lambda \Pi$ -исчисление . В: Г. Юэ и Г. Плоткин (редакторы), Логические структуры, издательство Кембриджского университета, 1991.
Дидье Гальмиш и Дэвид Пим. Поиск доказательств в теоретико-типических языках: введение . Теоретическая информатика 232 (2000) 5-53.
Филиппа Гарднер. Представление логики в теории типов . Технический отчет, Эдинбургский университет, 1992 г. Отчет LFCS ECS-LFCS-92-227.
Жиль Доук. Неразрешимость типизации в лямбда-пи-исчислении . В М. Беземе, Дж. Ф. Грооте (ред.), Типизированные лямбда-исчисления и приложения. Том 664 конспектов лекций по информатике , 139–145, 1993.
Дэвид Пим. Доказательства, поиск и вычисления в общей логике . Кандидат наук. диссертация, Эдинбургский университет, 1990 г.
Дэвид Пим. Алгоритм объединения $\lambda \Pi$ -исчисление. Международный журнал основ компьютерных наук 3 (3), 333–378, 1992.

Внешние ссылки [ править ]

Конкретные логические структуры и реализации (список ведется Фрэнком Пфеннингом , но в основном мертвые ссылки 1997 года)

[Jacobs2001-1] Перейти обратно: ^а ^б Барт Джейкобс (2001). Категориальная логика и теория типов . Эльзевир. п. 598. ИСБН 978-0-444-50853-9 .

[Gabbay1994-2] Дов М. Габбай, изд. (1994). Что такое логическая система? . Кларендон Пресс . п. 382. ИСБН 978-0-19-853859-2 .

[BoveBarbosa2009-3] Ана Бове; Луис Соареш Барбоза; Альберто Пардо (2009). Языковая инженерия и тщательная разработка программного обеспечения: Международная летняя школа LerNet ALFA 2008, Пириаполис, Уругвай, 24 февраля - 1 марта 2008 г., переработанная версия, избранные статьи . Спрингер. п. 48. ИСБН 978-3-642-03152-6 .

[1]

[2]

[3]