¬
( p q r s )

Examples

Grammar

Atomic formulas consist of a Latin letter optionally followed by more letters or digits. Exception: The English names of connectives (not, and, or, implies, iff) are reserved words and cannot be used as atomic formulas. Also note that the letter v is distinct from the connective .

If φ and ψ are formulas, then so are ¬φ, (φ∧ψ), (φ∨ψ), (φ→ψ), (φ↔ψ).

Several notations for connectives are supported:

Negation¬-not
Conjunction&and
Disjunction|or
Conditional->implies
Biconditional<->iff

Connectives are listed in decreasing order of precedence. All binary connectives are left-associative.