1955年~1956年に、アレン・ニューウェルハーバート・サイモン、J・C・ショーが開発したコンピュータプログラム。
「世界初の人工知能プログラム」といわれる。

数学の定理を証明することができる。
コンピュータが四則演算などの数値計算しかできなかった当時においては、画期的だった。