Książka porusza podstawy automatycznego dowodzenia twierdzeń matematycznych, a ściślej tego, co dziś nazywa się zautomatyzowanym rozumowaniem. Jest to pozycja już wiekowa, zawierająca wiele naiwnych koncepcji oraz charakteryzująca się dużą dozą ostrożności w przewidywaniach. Posiada jednak walory edukacyjne, z których najważniejszym jest syntetyczne i zwięzłe przedstawienie koncepcji rozkładu twierdzeń logiki, aż do ich aksjomatycznych podstaw. Jest to niewątpliwie plus w stosunku do publikacji dzisiejszych, w których temat ten ginie w gąszczu współczesnych struktur danych oraz wątków pobocznych, związanych z ewaluacją, analizą leksykalną i parsingiem.
Ciekawym, chociaż krótkim rozdziałem jest przedstawienie podstaw rachunku Gentzena. Niestety temat ten nie doczekał się w polskiej literaturze naukowej zbyt bogatej bazy.
Książkę można polecić głównie studentom oraz uczniom szkół średnich, aczkolwiek patyna czasu sprawia, że jest inspirująca nawet dla specjalistów pracujących w temacie.

Książka porusza podstawy automatycznego dowodzenia twierdzeń matematycznych, a ściślej tego, co dziś nazywa się zautomatyzowanym rozumowaniem. Jest to pozycja już wiekowa, zawierająca wiele naiwnych koncepcji oraz charakteryzująca się dużą dozą ostrożności w przewidywaniach. Posiada jednak walory edukacyjne, z których najważniejszym jest syntetyczne i zwięzłe przedstawienie...