Para entender o funcionamento deste método para testar a validade de argumentos clique aqui.

Além da lógica proposicional, este software permite testar a validade de argumentos da lógica de predicados e da lógica modal. Para isso, utilize os seguintes símbolos:

• (Ax) para ∀x,
• (Ex) para ∃x,
• + para □,
• * para ◇,
• também são permitidos códigos LaTeX.

Alguns exemplos de argumentos para utilizar neste software:

• (p→q), p : q - MODUS PONENS
• (p→q), ¬q : ¬p - MODUS TOLLENS
• (p→q), (q→r) : (p→r) - SILOGISMO HIPOTÉTICO
• (p ∨ q), ¬p : q - SILOGISMO DISJUNTIVO
• (¬(p ∨ q) ↔︎ (¬ p ∧ ¬ q)) - LEIS DE MORGAN
• ((p→q)↔︎(¬q→¬p)) - CONTRAPOSIÇÃO
• ◇p, (□p∨□¬p) : □p - ARG. ONTOLÓGICO MODAL
• (◇∃xFx→∃x◇Fx) - FÓRMULA DE BARCAN
• ∀x(Hx → Mx), Hs : Ms - (Todos os homens são mortais; Sócrates é homem; logo, Sócrates é mortal).