Основным недостатком программы РТТР является то, что пользователь должен отказаться от любых попыток взять на себя управление поиском решений. Каждое правило логического вывода в этой системе используется и в его первоначальной, и в кон-трапозитивной форме. Это может привести к выполнению таких операций поиска, которые противоречат здравому смыслу. Например, рассмотрим следующее правило:

Если бы оно рассматривалось как правило Prolog, то применялся бы разумный способ доказательства того, что два терма f равны. Но в системе РТТР должно быть также сформировано контрапозитивное правило:

По-видимому, попытка доказать, что любые два терма, x и а, являются разными, привела бы к непроизводительным затратам ресурсов.

Применение средств автоматического доказательства теорем в качестве помощников

До сих пор в этой книге любая система формирования рассуждений рассматривалась как независимый агент, который должен был принимать решения и действовать самостоятельно. Еще одно направление использования средств автоматического доказательства теорем состоит в том, что они должны служить в качестве помощников, предоставляя консультации, скажем, математикам. При эксплуатации подобных систем в режиме помощи математик действует в роли руководителя, очерчивая стратегию определения того, что должно быть сделано в следующую очередь, а затем передавая системе автоматического доказательства теорем просьбу проработать все детали. Это позволяет в определенной степени устранить проблему полуразрешимости, поскольку руководитель научной разработки может отменить запрос и опробовать другой подход, если поиск ответа на запрос потребовал слишком много времени. Любая система автоматического доказательства теорем может также действовать в качестве средства проверки доказательства; при ее использовании в таком режиме доказательство предоставляется человеком в виде ряда довольно крупных этапов; отдельные операции логического вывода, которые требуются для того, чтобы показать, что каждый из этих этапов является непротиворечивым, определяются системой.

В частности, сократовское средство формирования рассуждений (socratic reasoner) представляет собой такую систему автоматического доказательства теорем, в которой функция Ask является неполной, но эта система всегда позволяет прийти к определенному решению, если ей будет задан правильный ряд вопросов. Таким образом, сократовские средства формирования рассуждений становятся хорошими помощниками, при условии, что есть руководитель, способный составить правильный ряд вызовов функции Ask. Одной из сократовских систем формирования рассуждений для математиков является Ontic [1005].