Учебное заведение (информатика)
-
Определение и применение теории институтов
- Теория институтов была разработана для формализации логической системы.
- Институты позволяют разрабатывать языки спецификаций, математические доказательства и инструменты, независимые от базовой логической системы.
- Морфизмы связывают и переводят логические системы.
- Важными приложениями являются повторное использование логической структуры и разнородная спецификация логик.
-
Основные понятия теории институтов
- Модели и предложения рассматриваются как произвольные объекты, удовлетворяющие определённому бинарному отношению.
- Сигнатура определяет нелогичные символы, используемые в предложениях и моделях.
- Морфизмы сигнатур расширяют сигнатуры и сохраняют удовлетворенность предложений.
-
Формальное определение учреждения
- Учреждение состоит из категории подписей, функтора раздачи предложений, функтора редукции моделей и отношения удовлетворенности.
- Условие удовлетворенности гарантирует неизменность истины при изменении контекста.
-
Примеры учреждений
- Включают общую логику, CASL, логику первого порядка, логику высшего порядка, интуитивистскую логику, модальную логику, пропозициональную логику, временную логику и язык веб-онтологий OWL.
-
Рекомендации и библиография
- Статья является первой публикацией по теории институтов и предшественником работы Гогена и Берстолла.
- Включает обширную библиографию и ссылки на другие работы по теории институциональных моделей.