Эвристики для поиска доказательства

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

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

Стратегия поддержки. Для получения ответа на конкретный вопрос следует использовать конкретные факта из постановки задачи, а не только общие аксиомы. Можно принять, например, резолюцию к дизъюнктам (2.21) - (2.23) и получать все более общие теоремы о семейных отношениях, но это никогда не дало бы конкретного ответа. Для его получения придется использовать дизъюнкты (2.24) - (2.26) и их следствия. Прослеживая предшественников данного дизъюнкта в выводе, можно это обеспечить.

Выбор уникальных литер. В приведенном выше примере единственное вхождение предиката В без отрицания находится в дизъюнкте (2.23), поэтому ясно, что именно к нему должна применяя резолюция, в которой участвует ~В из (2.27). Напротив, ~F имеет много вхождений, поэтому лучше начать с резолюции по литерам вроде В. чтобы получить более короткие дизъюнкты, где вместо части переменных сделаны подстановки, что дает наводящие соображения для дальнейших подстановок.

Планирование. Человек обычно пытается спланировать доказательство, рисуя диаграммы и делая наброски доказательства прежде чем выписать все подробно. Может оказаться, что необходимо аксимотизировать информацию о том, какие аксиомы наиболее полезны. Это - метаинформация. Такой прием был успешно применен к Прологу для того, чтобы проводить доказательства в “пространстве планирования”, а затем использовать результаты для построения скелета доказательства и выбора использованных аксиом и подстановок, а также их порядка.