Запис атласу: https://www.aitimeline.dev/uk/events/evt-0103/
Дослідження · січень 1965 р.
Робінсон звів доведення в логіці першого порядку до одного правила виводу, придатного для машини.
Автоматичне доведення теорем стало реалізовним — і згодом перетворилося на логічне програмування.
Ключова частина — алгоритм уніфікації, що знаходить найзагальнішу підстановку для двох виразів. Метод працює через спростування: до множини тверджень додають заперечення цілі й шукають суперечність. Prolog 1972 року побудований на обмеженій формі цього ж механізму.
Випуск Journal of the ACM за січень 1965 року.
Journal of the ACM · Опубліковано січень 1965 р.
Communications of the ACM 31(1) (copy on the author's page at Imperial College) · Опубліковано 1988
Резолюція дала механізм виводу, якого бракувало системі advice taker.
Планування дій будувалося на доведенні теорем методом резолюції.
Замість повного логічного виводу дія описується списками додавання і видалення.
Стаття формулює результат саме про складність процедур доведення теорем.