Deduktívne systémy 2
Odvodzovacie pravidlá:
ak ?p, tak potom ?AGp (R1, zovšeobecnenie)
ak ?p a ?p ? q, tak potom ?q (R2, modus ponens)
Veta: Deduktívny systém s axiómami (Ax1)?(Ax11) a odvodzovacími pravidlami (R1), (R2) je sound (zdravý, korektný) and complete (úplný) pre CTL.