10.7. Проверка ограничений целостности

Проверку ограничений целостности можно осуществить с помощью двойной индукционной аксиомы второго порядка. Двойная индукционная аксиома очень похожа на простую индукционную аксиому и использует не одну, а две ситуационные переменные:

Двойная индукционная аксиома аналогична простой индукционной аксиоме. Так, для нашего примера со стипендиями студентов надо доказать истинность формулы

логически эквивалентной приведенной выше формуле, задающей ограничение целостности. Если обозначить

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

предположить истинность формулы На основании этого предположения показать, что истинна формула Переход

предположить истинность формулы На основании этого предположения показать, что истинна формула переход

если удастся доказать истинность всех этих формул, то сделать заключение, что имеет место истинность формулы что и требуется доказать.

Ограничение целостности является частным случаем ограничений на ситуации (состояния), которые формулируются с помощью индукционных аксиом различного типа. Индукционные аксиомы второго порядка могут быть использованы для определения свойств различных сред, в которых выразительных средств логики предикатов первого порядка недостаточно.

Вопросы и упражнения

(см. скан)