◀ اینجا می‌توانید دیسول‌های گویایی و انگارش را به‌سادگی بنویسید و آنها را در جاهای دیگر بکار برید.

نمونه‌ها:
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 \/ --phiIPC⊬𝜙∨¬𝜙
--phi =- phi -> _|¬𝜙≡𝜙→⊥
Gamma |= phi => Gamma |- phiΓ⊨𝜙⇒Γ⊢𝜙

◀ با فشردن دکمه ارزیابی می‌توانید بررسی کنید که دیسول(های) اندر شده یک دربرد پایمند می‌سازند یا نه.