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

نمونه‌ها:

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	➟	Γ⊨𝜙⇒Γ⊢𝜙

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