Интерполяция Крейга
-
Интерполяция Крейга
- Интерполяция Крейга — это метод доказательства непротиворечивости теорий, основанный на теореме Линдона.
- Теорема Линдона утверждает, что если теория S не выполнима, то существует интерполяционное предложение ρ, которое истинно в S и ложно в T.
- Интерполяционное предложение ρ имеет свойство, что каждый символ отношения в ρ имеет положительное значение в S и отрицательное значение в T.
-
Конструктивное доказательство интерполяционной теоремы Крейга
- Доказательство интерполяционной теоремы Крейга для пропозициональной логики представлено в статье.
- Интерполяция ρ удовлетворяет условиям φ → ρ и ρ → ψ, где атомы(φ) и атомы(θ) — наборы пропозициональных переменных.
- Доказательство проводится индукцией по числу переменных, не встречающихся в θ.
- Алгоритм вычисления интерполяций позволяет получить интерполянт с большим числом логических связей, чем исходное предложение φ.
-
Приложения интерполяции Крейга
- Интерполяция Крейга используется для доказательства непротиворечивости, проверки моделей, в модульных спецификациях и онтологиях.
-
Рекомендации
- Ссылки на статьи и диссертации для дальнейшего чтения предоставлены в конце статьи.