|
А8 . Inext (А лВ) О (next A) a (next В), когда ckA= ckB. A9. I□ □ A о □ A. A10.1first □ A cs> □ A. A11 .1next □ A о □ А, когда ckAбесконечная последовательность. A12. I□ (А лВ) о (□ А) л (пВ ), когда ckA= ckB. Правила вывода R I.E a ra A ^ В и I-А ,то I-В,когдаскАскв. R2. Если !•А , то Ifirst А , когда скА • не пустая последовательность. R3. Если IА , то Inext А , когда ск$д не пустая последовательность. R4. Если 1-А , то I□ А . Правило R1 можно рассматривать как аналог modens ponens, а правила R2 R4 будем называть временными операторами. Очевидно также следующее утверждение: аксиомы А1 • А 12 и правила R l R4 справедливы относительно семантической схемы для TLC. Дополнительно в TLC вводятся правила и формулы фиксированного времени. Правила фиксированного времени выводятся из правил вывода TLC и будут одними из основных конструкций предлагаемой ниже расширения TLC. Утверждается » что атом является атомом фиксированного времени, если к нему применяется оператор first после ряда применений оператора next. Любой атом фиксированного времени фиксирован в определенный момент времени на своих локальных часах, т.е. атомы фиксированного времени это атомы, значения которых зависят ровно от одного момента времени Определение 9, Пусть p(ei,...A ) * чистый атом, ск присваивание часов, скр • часы ассоциированные с р на ск. Если teck(p) и rank (t, скр) = п, где п натуральное число, то будем называть first next [n ] p(ei,—A ) атомом фиксированного времени, a ckpw ,т.е.?t текущим временем атома р(е,...А ) относительно атома фиксированного времени. |
All. Inext □ A о □ А, когда ckAбесконечная последовательность . A12. I□ (А лВ) о (□ А) л (QB), когда ckA= ckB. Правила вывода R1. Если A -> В и 1 -A , то IВ, когда ckA= ckB. R2. Если IA , то Ifirst A , когда ckAне пустая последовательность. R3. Если IА , то Inext А, когда скФ Ане пустая последовательность. R4. Если 1 -А , то I□ А . Правило R1 можно рассматривать как аналог modens ponens, а правила R2 R4 будем называть временными операторами. Очевидно также следующее утверждение: аксиомы А1 А12 и правила Rl R4 справедливы относительно семантической схемы для TLC. Дополнительно в TLC вводятся правила и формулы фиксированного времени. Правила фиксированного времени выводятся из правил вывода TLC и будут одними из основных конструкций предлагаемой ниже расширения TLC. Утверждается , что атом является атомом фиксированного времени, если к нему применяется оператор first после ряда применений оператора next. Любой атом фиксированного времени фиксирован в определенный момент времени на своих локальных часах, т.е. атомы фиксированного времени это атомы, значения которых зависят ровно от одного момента времени Определение 9. Пусть p(ei,...,ek) чистый атом, ск присваивание часов, скрчасы ассоциированные с р на ск. Если teck(p) и rank (t, скр) = п, где п натуральное число, то будем называть first next [n ] p(ei,...,ek) атомом фиксированного времени, a ckp(n) ,т.е., t текущим временем атома p(ei,...,ek) относительно атома фиксированного времени. 94 |