Theorems about unless
Reflexívnost a antireflexívnost:
Dôkaz: {false} S {p}, {p} S {true} pre ?S
Zoslabenie:
p unless q, q ? r / p unless r
Dôkaz:
{p ? ?q} S {p ? q}. Z q ? r, ?r ? ?q a teda
p ? ?r ? p ? ?q
p ? q ? p ? r a teda
{p ? ?r} S {p ? r}, cize „p unless r”.
Disjukcia
p unless q, p’ unless q’ /
/ (p ? p’) unless (? p ? q’) ? (? p’ ? q) ? (q ? q’)
Konjunkcia
p unless q, p’ unless q’ /
/ (p ? p’) unless (p ? q’) ? (p’ ? q) ? (q ? q’)
Dôkaz: ? a ? môzu byt aplikované na post- a pre-conditions, teda
{(p ? ?q) ? (p’ ? ?q’)} S {(p ? q) ? (p’ ? q’)},
potom pouzit pravidlo
p’ ? p, q ? q’, {p} S {q} / {p’} S {q’}