(theorem prover)
narzedzie, w którym do automatyzacji wiekszosci zabiegów recznego dowodzenia stosuje sie m e t o d y h e u r y s t y c z n e. Dowodzenie twierdzen jest zbyt kosztowne, aby w perspektywie najblizszych lat obsluzyc je za pomoca kompilatora produkcyjnego - wymaga ono asysty ze strony eksperta. Zob. tez heurystyka, produkcja gramatyki.