Алгебра Роббинса
В абстрактной алгебре алгебра Роббинса представляет собой алгебру , содержащую одну бинарную операцию , обычно обозначаемую как , и одну унарную операцию , обычно обозначаемую как . Эти операции удовлетворяют следующим аксиомам :
В течение многих лет предполагалось, но не было доказано, что все алгебры Роббинса являются булевыми алгебрами . Это было доказано в 1996 году, поэтому термин «алгебра Роббинса» теперь является просто синонимом «булевой алгебры».
В 1933 году Эдвард Хантингтон предложил новый набор аксиом для булевых алгебр, состоящий из (1) и (2) выше, а также:
Вскоре после этого Герберт Роббинс выдвинул гипотезу Роббинса , а именно, что уравнение Хантингтона можно заменить тем, что стало называться уравнением Роббинса, и в результате получится булева алгебра . будет интерпретировать логическое соединение и логическое дополнение . Булева встреча , а константы 0 и 1 легко определяются из примитивов алгебры Роббинса. В ожидании проверки гипотезы система Роббинса получила название «алгебра Роббинса».
Проверка гипотезы Роббинса требовала доказательства уравнения Хантингтона или какой-либо другой аксиоматизации булевой алгебры как теорем алгебры Роббинса. Хантингтон, Роббинс, Альфред Тарский и другие работали над проблемой, но не смогли найти ни доказательства, ни контрпримера.
Уильям МакКьюн доказал эту гипотезу в 1996 году с помощью автоматизированного средства доказательства теорем EQP . Полное доказательство гипотезы Роббинса в одной последовательной системе обозначений и внимательном следовании МакКьюну см. в Mann (2003). Дан (1998) упростил машинное доказательство МакКьюна.