Дослідження · січень 1965 р.
Робінсон звів доведення в логіці першого порядку до одного правила виводу, придатного для машини.
Автоматичне доведення теорем стало реалізовним — і згодом перетворилося на логічне програмування.
Ключова частина — алгоритм уніфікації, що знаходить найзагальнішу підстановку для двох виразів. Метод працює через спростування: до множини тверджень додають заперечення цілі й шукають суперечність. Prolog 1972 року побудований на обмеженій формі цього ж механізму.
Випуск Journal of the ACM за січень 1965 року.
Journal of the ACM · Опубліковано січень 1965 р.
Резолюція дала механізм виводу, якого бракувало системі advice taker.
Планування дій будувалося на доведенні теорем методом резолюції.
A Mobile Automaton: An Application of Artificial Intelligence TechniquesЗамість повного логічного виводу дія описується списками додавання і видалення.
STRIPS: A New Approach to the Application of Theorem Proving to Problem SolvingСтаття формулює результат саме про складність процедур доведення теорем.