Geometry Theorem Prover - geometriai tételbizonyító program

Rövid szöveges bemutatás: 
A geometriai tételbizonyító rendszert Gelernter hozta létre 1959-ben, a szabadidejében, miközben főállásban az IBM-nél készített egyéb rendszereket. A tételbizonyító képes volt az akkori középiskolai matematikai geometriai tételek bizonyítására. A rendszer speciális heurisztikák alapján működött és visszalépéses láncolt keresést használt. Fő heurisztikaként olyan diagramokat használt, mely követte a bizonyítással járó állításokat, így tudta elkerülni a hamis cél állításokat.