¬
∧
∨
→
↔

(
p
q
r
s
)

### Examples

- ¬p∧q↔¬p
- p∧q∨s∧r↔s→r∧(q∨p)
- -p->-q<->q|p->-p

### 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.