Искусственный интеллект

9.9. Доказательство свойств корректности Из материала настоящей главы ясно, что временная модальная логика является одним из видов ситуационного исчисления. Интерпретация формул этой логики осуществляется посредством логики предикатов первого порядка. Принципы доказательства в модальной логике те же, что и для других исчислений, базирующихся на логике предикатов первого порядка. Единственное отличие состоит в использовании при доказательстве-правил и формул, содержащих модальные операторы. Для доказательства свойств корректности нам необходимо иметь следующие исходные данные. Аксиомы собственно модальной логики, часть из которых была рассмотрена в начале настоящей главы. Эти аксиомы, как обычно, назовем базовыми аксиомами.