Processing math: 100%

Table of Contents

Syntax | Terms | Equations | Horn formulas | Universal formulas | First-order formulas | Theories

Variables

x y z u v w x0 x1 x2

Operation symbols

Relation symbols

Connectives

Quantifiers

Delimiters

Signatures / Languages

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.