symbol	type	comment
∧	/\
∨	\/
¬	!
F	FF
T	TT
U	UU
→	-->
↔	<->
&&	&&	short-circuit and
||	||	short-circuit or
↠	->>	Łukasiewicz implication (not yet implemented)
*	*	is defined (not yet implemented)

symbol	type
∀ x:	AA x:
∀ x; 0 ≤ x < y:	AA x; 0 <= x < y:
∃ x:	EE x:
∃ x; x + 2 ≠ z:	EE x; x+2 != z:

(Between ; and :, not all operators are available)

symbol	type	comment
⇒	==>
⇐	<==
⇔	<=>	unifies U and F
≡	===	does not unify U and F

A global assumption (i.e., axiom) may be added to the front, e.g.: assume x > 3 \/ x = y;

symbol	type
<	<
≤	<=
=	=
≠	!=
≥	>=
>	>

symbol	type
+	+
−	-
3y	3y
y ⋅ 3	y*3
|2x − 5|	|2x-5|
x + 1 6	(x+1)/6
2 3 4	2 3/4
x div 3	y div 3
x mod 3	x mod 3
(3 + 4)(x + 5) div (1+2)	(3+4)(x+5) div (1+2)