Эквивалентное доказательство
Эта статья может чрезмерно полагаться на источники, слишком тесно связанные с предметом , что потенциально препятствует тому, чтобы статья была проверяемой и нейтральной . ( Март 2024 г. ) |
EQP ( Уравненное доказательство ) — это автоматизированная программа доказательства теорем для эквациональной логики , разработанная Отделением математики и информатики Аргоннской национальной лаборатории . Это был один из доказывающих, используемых для решения давней проблемы, поставленной Гербертом Роббинсом , а именно: все ли алгебры Роббинса являются булевыми алгебрами .