Без заголовка

В книге Гутер Р., Полунов Ю. "Математические машины" приводится пример теоремы, впервые доказанной компьютером Возможно, тут подойдет полный перебор взаимосвязей между терминами на определенную глубину (1-2-3-4х - ходовки) из перечислений всех комбинаций приемов с помощью машины, аналогичной Прологу (https://github.com/raydac/jprol из raydac в http://ru-declarative.livejournal.com/112145.html ) На нереальные комбинации можно ставить фильтры, хотя, IMHO, проверить ограничение полетов мысли соседними/абстрактносимметричными уровнями сложности - не помешает N.B. А книга замечательная! Добавить в хвост комментарии про современную элементную базу, и переиздать!