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

Теория SOrdp

Теория SOrdp – теория предпорядка на множествах в языке LSO с алфавитом ASO и классом ППТ CST. .

Правила вывода:

Правило modus ponens (правило отделения): ((AB), A) => B.

Определение класса ППТ CST:
CST={S₁, P₁, Q₁, M₁, S₂, P₂, Q₂, M₂, ..., S_n, P_n, Q_n, M_n, ...}.

Определение класса ППФ LSO:
1) (t₁, t₂ є CST) => ((t₁t₂) є LPO;
2) (A, B є LPO) => (¬A, (A&B), (AB), (AB), (AB) є LPO).