Такое доказательство действительно отвечает на вопрос "Действительно ли этого кота убило Любопытство?", но часто требуется найти ответ на более общие вопросы, такие как "Кто убил кота?" Резолюция позволяет это сделать, но для получения ответа требует немного больше работы. Данная цель может быть представлена в виде выражения, которое после его отрицания принимает в форме

CNF вид. Повторяя доказательство, показанное на рис. 9.8, с новой отрицаемой целью, мы получим аналогичное дерево доказательства, но с подстановкой {w/Curiosity} в одном из этапов. Поэтому в данном случае для поиска того, кто убил кота, достаточно проследить за связываниями, которые применяются к переменным запроса в этом доказательстве.

К сожалению, в методе резолюции могут вырабатываться неконструктивные доказательства для существующих целей. Например, в выражении после применения операции резолюции удаляется взаимно дополнительный литерал, входящий в состав выражения, с получением выражения Kills {Jack, Tuna), к которому снова применяется операция резолюции с использованием выражения, что приводит к получению пустого выражения. Обратите внимание на то, что в этом доказательстве переменная w имеет два различных связывания, а правило резолюции сообщает нам, что кто-то действительно убил кота Тунца — либо Джек, либо Любопытство. Но в этом для нас нет ничего нового! Одно из решений данной проблемы состоит в том, чтобы регламентировать допустимые этапы резолюции так, чтобы переменные запроса могли быть связанными только один раз в каждом конкретном доказательстве; в таком случае можно будет предусмотреть применение перехода с возвратом по всем возможным связываниям. Еще одно решение состоит в добавлении специального литерала ответа к отрицаемой цели, которая принимает вид. Теперь процесс резолюции вырабатывает ответ каждый раз, когда формируется выражение, содержащее только единственный литерал ответа. Для доказательства, приведенного на рис. 9.8, таковым является выражение Answer (Curiosity). Неконструктивное доказательство привело бы к выработке выражения, которое не может рассматриваться как ответ и отбрасывается.