Средства автоматического доказательства теорем (называемые также средствами автоматизированного формирования рассуждений) отличаются от языков логического программирования в двух отношениях. Во-первых, большинство языков логического программирования поддерживает только хорновские выражения, тогда как средства автоматического доказательства теорем поддерживают полную логику первого порядка. Во-вторых, в программах на таком типичном языке логического программирования, как Prolog, переплетаются логика и управление. Например, выбор программистом выражения А : - в, С вместо А : - С, в может повлиять на выполнение программы. С другой стороны, в большинстве средств автоматического доказательства теорем синтаксическая форма, выбранная для высказываний, не влияет на результаты. Для средств автоматического доказательства теорем все еще требуется управляющая информации, чтобы они могли функционировать эффективно, но эта информация обычно хранится отдельно от базы знаний, а не входит в состав самого представления знаний. Большинство исследований в области средств автоматического доказательства теорем посвящено поиску стратегий управления, которые приводят к общему повышению эффективности, а не только к увеличению быстродействия.

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

В этом разделе описана программа автоматического доказательства теорем Otter (Organized Techniques for Theorem-proving and Effective Research) [1018]; в этом описании особое внимание будет уделено применяемой в ней стратегии управления. Подготавливая любую задачу для программы Otter, пользователь должен разделить знания на четыре описанные ниже части.

•    Множество выражений, известное как множество поддержки (или sos — set of support), в котором определяются важные факты о данной задаче. На каждом этапе резолюции операция резолюции применяется к одному из элементов множества поддержки и к другой аксиоме, поэтому поиск сосредоточивается на множестве поддержки.

•    Множество полезных аксиом (usable axiom), которое выходит за пределы множества поддержки. Эти аксиомы предоставляют фоновые знания о проблемной области. Определение границы между тем, что должно войти в состав задачи (и поэтому в множество sos) и что относится к фоновым знаниям (и поэтому должно войти в число полезных аксиом), передается на усмотрение пользователя.