Короткий ответ:
Да, обе формулы эквивалентны, и вы можете переписать Fp также с помощью (¬p)Up.
и доказательство:
Мы можем исследовать проблему, взглянув на определение pUq (я думаю, что оно определено таким образом в книге «Проверка модели» Кларка, Грумберга, Пеледа).
Путь s является моделью для формулы (обозначается s ⊨ pUq):
s ⊨ pUq <=> ∃k: s^k ⊨ q
∧ ∀i: 0<=i<k => s^i ⊨ q
(С s^i это путь s с удаленными первыми i шагами.)
У нас есть (1):
s ⊨ (¬p)Up <=> ∃k: s^k ⊨ p
∧ ∀i: 0<=i<k => s^i ⊨ ¬p
и (2):
s ⊨ TUp <=> ∃k: s^k ⊨ p
∧ ∀i: 0<=i<k => s^i ⊨ true
<=> ∃k: s^k ⊨ p
Мы хотим показать (1) ‹=> (2) (я переименовал ks в k1 и k2, чтобы избежать путаницы):
∃k1: s^k1 ⊨ p
∧ ∀i: 0<=i<k1 => s^i ⊨ ¬p
<=>
∃k2: s^k2 ⊨ p
Направление (1) => (2) тривиально.
Для (2) => (1) нужно показать, что из
∃k2: s^k2 ⊨ p
следует
∃k1: s^k1 ⊨ p ∧ ∀i: 0<=i<k1 => s^i ⊨ ¬p
Мы знаем, что существует значение для k1 (а именно k2), такое, что выполняется s^k1 ⊨ p. Но как насчет второй части? Теперь мы можем просто использовать для k1 наименьшее значение, которое соответствует s^i ⊨ p. Тогда вторая часть верна, потому что если бы существовало i такое, что s^i ⊨ not p не выполняется, мы знаем, что выполняется s^i |= p. Но в этом случае мы бы выбрали i вместо k1, потому что i строго меньше, чем k1.
Таким образом, обе формулы (1) и (2) эквивалентны.
person
danielp
schedule
12.06.2015
