/* В этой онтологии вводится грамматика булевых выражений в форме Бэкуса-Наура */.
Бул_выр ::= "Конъюнкт | Бул_выр 'V' Конъюнкт".
Конъюнкт ::= "Атом | Конъюнкт '&' Атом".
Атом ::= " 'f' | 't' | '(' Бул_выр ')' | '~'Атом | Бул_переменная ".
/* Соотношения */.
~f=t. ~t=f.
f V f = f. f v t = t. t v f = t. t v t = t.
f & f = f. f & t = f. t & f = f. t & t = t.
(t)=t. (f)=f.
/* Правила переписывания */.
Для всех [u:Бул_выр] [ u V t] => [ t ] ("Дизъюнкция с t справа").
Для всех [u:Конъюнкт] [ t V u] => [ t ] ("Дизъюнкция с t слева").
Для всех [u:Конъюнкт] [ u & t] => [ u ] ("Конъюнкция с t справа").
Для всех [u:Атом] [ t & u] => [ u ] ("Конъюнкция с t слева").
Для всех [u:Атом] [ u & u ] => [ u ] ("Идемпотентность конъюнкции").
Для всех [u1:Конъюнкт; u:Атом] [u1 & u & u ] => [ u1 & u ] ("Идемпотентность конъюнкции справа").
Для всех [u:Конъюнкт] [ u V u ] => [ u ] ("Идемпотентность дизъюнкции").
Для всех [u1:Бул_выр; u:Конъюнкт] [u1 V u V u ] => [ u1 V u ] ("Идемпотентность дизъюнкции справа").
Для всех [u1:Бул_выр; u2:Конъюнкт] [ ~(u1 V u2)] => [(~(u1) & ~(u2))] ("ДеМорган дизъюнкции").
Для всех [u1:Конъюнкт; u2:Атом] [ ~(u1 & u2)] => [(~(u1) V ~(u2))] ("ДеМорган дизъюнкции").
Для всех [u:Атом] [ ~~u ] => [ u ] ("Двойное отрицание").
Для всех [u:Атом] [ (u) ] => [ u ] ("Убраны скобки").
Для всех [u1:Бул_выр; u2:Конъюнкт; u3:Конъюнкт] [ u3&(u1 V u2)] => [(u3&(u1) V u3&(u2))] ("Дистрибутивность слева").
Для всех [u1:Бул_выр; u2:Конъюнкт; u3:Атом] [ (u1 V u2)&u3 ] => [((u1)&u3 V u2&u3)] ("Дистрибутивность справа").
Для всех [u1:Бул_выр; u2:Конъюнкт; u3:Конъюнкт] [ (u1 V u2) V u3 ] => [(u1) V u2 V u3] ("Скобка , дизъюнкция").
Для всех [u1:Бул_выр; u2:Бул_выр; u3:Конъюнкт] [ u1 V (u2 V u3) ] => [u1 V (u2) V u3] ("Скобка , дизъюнкция").
Для всех [u1:Конъюнкт; u2:Атом; u3:Атом] [ (u1 & u2) & u3 ] => [(u1) & u2 & u3] ("Скобка , конъюнкция").
Для всех [u1:Конъюнкт; u2:Конъюнкт; u3:Атом] [ u1 & (u2 & u3) ] => [(u1 & (u2) & u3)] ("Скобка , конъюнкция").
Для всех [u1:Конъюнкт; u2:Атом; u3:Конъюнкт] [ (u1 & u2) V u3 ] => [u1 & u2 V u3] ("Скобка , кон_дизъюнкция").
Для всех [u1:Бул_выр; u2:Конъюнкт; u3:Атом] [ u1 V (u2 & u3) ] => [(u1) V u2 & u3] ("Скобка , диз_конъюнкция").