Информационная система по формальным теориям

Алфавит AQPr языка

Элементарные константные термы:
a₁, b₁, c₁, d₁, a₂, b₂, c₂, d₂, ..., a_n, b_n, c_n, d_n, ... – символы для простых сингулярных термов.

Элементарные переменные термы:
x₁, y₁, z₁, x₂, y₂, z₂, ..., x_n, y_n, z_n, ... – индивидные переменные термы.

Функторы:
fⁿ¹₁, gⁿ²₁, hⁿ³₁, fⁿ⁴₂, gⁿ⁵₂, hⁿ⁶₂, ..., f^nk1_n, g^nk2_n, h^nk3_n, ... – символы для функциональных констант.

Предикаторы:
Qⁿ¹₁, Rⁿ²₁, Pⁿ³₁, Sⁿ⁴₁, Qⁿ⁵₂, Rⁿ⁶₂, Pⁿ⁷₂, Sⁿ⁸₂, ..., Q^nk1_n, R^nk2_n, P^nk3_n, S^nk4_n, ... – символы для предикатных констант.

Кванторы
1) – квантор всеобщности;
2) – квантор существования.

Пропозициональные связки:
1) ¬ – отрицание;
2) & – конъюнкция;
3) – дизъюнкция;
4) – импликация;
5) – эквивалентность.

Технические знаки:
( – левая и
) – правая скобки.