СЕКВЕНЦИАЛЬНОЕ ИСЧИСЛЕНИЕ
----------------------------------------------------------------------------
     Аксиома СЕКВЕНЦИАЛЬНОГО ВЫВОДА.
     F1, L -> R, F1
----------------------------------------------------------------------------
     Правила СЕКВЕНЦИАЛЬНОГО ВЫВОДА.
Конъюнкция:
           F1,F2,L->R                   L->R,F1   L->R,F2
    (&<-)  ----------            (->&)  -----------------
           F1&F2,L->R                      L->R,F1&F2

Дизъюнкция:
           F1,L->R   F2,L->R            L->R,F1,F2
    (V<-)  -----------------     (->V)  ----------
              F1VF2,L->R                L->R,F1VF2

Импликация:
           L->R,F1   F2,L->R            F1,L->R,F2
    (><-)  -----------------     (->>)  ----------
              F1>F2,L->R                L->R,F1>F2

Отрицание:
            L->R,F1                     F1,L->R
    (┐<-)  --------              (->┐)  --------
           ┐F1,L->R                     L->R,┐F1

Кванторы:
           A.vF1,(Svt)F1,L->R           L->R,(Svw)F1
    (A<-)  ------------------    (->A)  ------------
               A.vF1,L->R                L->R,A.vF1

           (Svw)F1,L->R                L->R,(Svt)F1,E.vF1
    (E<-)  ------------          (->E) ------------------
            E.vF1,L->R                     L->R,E.vF1

Обозначения:
     F1 и F2 - формулы, L и R - списки формул;
     w - константа,  не встречающаяся в заключениях правил ->A и  E<-;
     t - терм,  свободный для v в F1;
     (Sxy)F1 - подстановка: в F1 заменить x на y.
----------------------------------------------------------------------------