Equational logic

First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol. The model theory of this logic was developed into Universal algebra by Birkhoff, Grätzer and Cohn. It was later made into a branch of category theory by Lawvere ("algebraic theories").

The terms of equational logic are built up from variables and constants using function symbols (or operations).

Here are the four inference rules of logic ${\textstyle E}$. ${\textstyle P[x:=E]}$ denotes textual substitution of expression ${\textstyle E}$ for variable ${\textstyle x}$ in expression ${\textstyle P}$. ${\textstyle b=c}$ denotes equality, for ${\textstyle b}$ and ${\textstyle c}$ of the same type, while ${\textstyle b\equiv c}$, or equivalence, is defined only for ${\textstyle b}$ and ${\textstyle c}$ of type boolean. For ${\textstyle b}$ and ${\textstyle c}$ of type boolean, ${\textstyle b=c}$ and ${\textstyle b\equiv c}$ have the same meaning.

...
Wikipedia