◀ اینجا میتوانید دیسولهای گویایی و انگارش را بهسادگی بنویسید و آنها را در جاهای دیگر بکار برید.
نمونهها:
forall S forsome P forall x(x elem P <=> x psubset S) | ➟ | ∀S ∃P ∀x(x∈P⇔x⊂S) |
[](p-)q)-)<>(p-)q) | ➟ | ◻(p⊃q)⊃◇(p⊃q) |
IPC |/- phi \/ --phi | ➟ | IPC⊬𝜙∨¬𝜙 |
--phi =- phi -> _| | ➟ | ¬𝜙≡𝜙→⊥ |
Gamma |= phi => Gamma |- phi | ➟ | Γ⊨𝜙⇒Γ⊢𝜙 |
◀ با فشردن دکمه ارزیابی میتوانید بررسی کنید که دیسول(های) اندر شده یک دربرد پایمند میسازند یا نه.