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

Выражения вида У w служат базовыми утверждениями свойств программы (теоремами). Главной нашей целью является составление таких формул (теорем) и рассмотрение процедур доказательства их истинности. Разработчик программ, желающий убедиться, что его программы удовлетворяют определенным свойствам, должен сформулировать эти свойства, а затем доказать их. 196 9.6. Инвариантные свойства Для дальнейшего рассмотрения важно следующее справедливое утверждение: \= w з N w. Оно означает, что если w истинна для любой возможной последовательности, то она истинна также для каждого (Р, ф)-вычисления. Это утверждение позволяет нам записать общезначимые формулы временной модальной логики \= w с использованием введенного обозначения N : Н П -1 ws-IOw, N П(и>, э w2) э (Dn>, => Dw2), N D(»v z> ° w) 3 (w э Dw). Справедливым является также следующее выражение: