Syntax | Terms | Equations | Horn formulas | Universal formulas | First-order formulas | Theories
x y z u v w x0 x1 x2 …
A signature or language is a sequence of operation symbols, relation symbols and connectives.
Prefix symbols always apply first. Infix symbols and postfix symbols can
In a typed (or multisorted) language the input/output slots of operation symbols and relation symbols are associated to a specific type.
In an order-sorted language the types form a partially ordered set that determines the subtyping relation.