|
Содержательно это означает, что □ А истинно в момент времени t на локальных часах скА только в случае, если А истинно во все моменты времени на скА. Семантика связок v> — О , квантора В очевидным образом может быть получена из определений ( 1 )... (8 ). (9) Для каждого t€ ckA, К лал ФА, если и только если К ла.»A se ckA. Определение (9) следует из определений (3) и (8 ), а содержательно оно означает, что ОА истинно в момент времени t на локальных часах скА в случае, если А истинно в некоторый момент времени на скА. Система доказательства в TLC вводится следующим образом. Система доказательства содержит множество аксиом и множество правил вывода. Помимо аксиом логики первого порядка в TLC имеются приведенные ниже аксиомы и правила вывода, связанные с временными операторами и присваиванием часов. Отметим также, что используемая в этих аксиомах нотация 1А означает, что А является теоремой TLC, т.е. формула А истинна для всех моментов времени на локальных часах, ассоциированных с данной формулой при любом присваивании часов. Заметим, что это не обязательно означает, что А истинна для всех моментов времени вообще на любых часах. Другими словами, !• А означает К и А, т.е. А есть теорема, которая истинна на локальных часах скАдля любого присваивания часов ск. Аксиомы A l. Ifirst first А о first А. А2. 1next first А о first А, ели скАбесконечная последовательность АЗ. \first А « 1 (first А). А4. Inext А о -t (next А). А5. Ifirst (Vx) А о (Vx) (first А). Аб. next (Vx) А о (Vx) (next А). А7. Ifirst (А лВ) О (first А) л (first В), когда ckAl0) “ ckB<0). 157 |
Определение (9) следует из определений (3) и (8 ), а содержательно оно означает, что ОА истинно в момент времени t на локальных часах скЛ в случае, если А истинно в некоторый момент времени на скА. Система доказательства в TLC вводится следующим образом. Система доказательства содержит множество аксиом и множество правил вывода. Помимо аксиом логики первого порядка в TLC имеются приведенные ниже аксиомы и правила вывода, связанные с временными операторами и присваиванием часов. Отметим также, что используемая в этих аксиомах нотация IА означает, что А является теоремой TLC, т.е. формула А истинна для всех моментов времени на локальных часах, ассоциированных с данной формулой при любом присваивании часов. Заметим, что это не обязательно означает, что А истинна для всех моментов времени вообще на любых часах. Другими словами, 1 А означает l=C ki А, т.е. А есть теорема, которая истинна на локальных часах скЛ для любого присваивания часов ск. Аксиомы А1. Ifirst first А <=>first А. A l. 1 next first A о first А, ели ckAбесконечная последовательность АЗ. Ifirst -i A <=>-i (first A). A4. 1 nextl A o i (nextA). A5. Ifirst (Vx) A <=>(Vx) (first A). A6 . Inext (Vx) A <=>(Vx) (next A). A7. Ifirst (А дВ) о (first А) д (firstВ),когда ckA < 0 )= ckB (0). A8 . Inext (А лВ) <=>(next А) л (next В), когда ckA=ckB. A9. I□ □ A о □ A. A 10.1 first щ А о q A. 93 |