ГОСТ Р 56271-2014
П р и м е р — Множество шаблонов:
{ А(х) *-*3y.(6(y)AR(x.y)).
В(х) <->C(x)vD(x)}.
AiaUBib
расширено до формулы А(а)/В(Ь) в виде:
3y.(8i^-
)
R(a.y))AS(b)
3y.(C(y)vD(y))AR(&y))A^bi
-^3y.(C(y)vD<y))AR(a.y))A(C(6)vD(b))
где расширенные под-формулы подчеркнуты, или в виде:
А(а)лЩ)
ЗуАВ(у),-.Ша.у))лВ(Ь)
-о 3y.(S(y), R(a.y))A(C(b)AD(b)
-^3y.((C(y)vD(y))AR(a.y))A(C(b)vD(b))
или окончательно в виде:
А(а)лВ(Ь)
^AMMC(bUDlb)
^ 3y.(8£yi‘.R(a.y))A(C(b)vD(6))
^3y.((C(y)vD(y))AR(a.y))A(C(b)vD(b))
Видно, что получился тот же результат.
J.3 Расширение шаблона
Для множества шаблонов Se T S ^) и формулы 0 типал-у-3 над символами во множестве I^nam es^).
определено расширение 0 по отношению к S как нормальной формы о для R(S). Это есть уникально определен
ный результат последовательного применения правил переписывания из R(S) к
89