Boyer–Moore-tételbizonyító

Kapcsolódó fogalmak: 
elsőrendű logika
Rövid szöveges bemutatás: 
Boyer–Moore-tételbizonyítót 1979-ben alkotta meg Boyer és Moore. Automatikus volt, elsőrendű logikát használt és célja a bizonyítás megoldása volt. Segítségével újszerű matematikai eredményeket produkáltak.