En álgebra abstracta , un álgebra de Robbins es un álgebra que contiene una única operación binaria , normalmente denotada por , y una única operación unaria normalmente denotada por satisfaciendo los siguientes axiomas :
Para todos los elementos a , b y c :
Durante muchos años se ha conjeturado, aunque no se ha demostrado, que todas las álgebras de Robbins son álgebras de Boole . Esto se demostró en 1996, por lo que el término "álgebra de Robbins" es ahora simplemente un sinónimo de "álgebra de Boole".
En 1933, Edward Huntington propuso un nuevo conjunto de axiomas para las álgebras de Boole, que consta de (1) y (2) anteriores, más:
A partir de estos axiomas, Huntington derivó los axiomas habituales del álgebra de Boole.
Muy poco después, Herbert Robbins planteó la conjetura de Robbins , es decir, que la ecuación de Huntington podía sustituirse por lo que se dio en llamar la ecuación de Robbins, y el resultado seguiría siendo el álgebra de Boole . interpretaría la unión booleana y el complemento booleano . La unión booleana y las constantes 0 y 1 se definen fácilmente a partir de las primitivas del álgebra de Robbins. A la espera de la verificación de la conjetura, el sistema de Robbins se denominó "álgebra de Robbins".
Para verificar la conjetura de Robbins era necesario demostrar la ecuación de Huntington, o alguna otra axiomatización de un álgebra de Boole, como teoremas de un álgebra de Robbins. Huntington, Robbins, Alfred Tarski y otros trabajaron en el problema, pero no lograron encontrar una prueba o un contraejemplo.
William McCune demostró la conjetura en 1996, utilizando el demostrador automático de teoremas EQP . Para una demostración completa de la conjetura de Robbins en una notación coherente y siguiendo de cerca a McCune, véase Mann (2003). Dahn (1998) simplificó la demostración de McCune.
