Процедура Девіса — Патнема з розщепленням
У звіті Нью-Йоркського університету від 8 червня 1961 року Мартін Девіс, Джордж Логеман і Дональд Лавленд описали програму для IBM 704, що перевіряє формули методом Девіса й Патнема 1960 року, замінивши одне з його правил правилом розщеплення. Формулу, над якою програма Гілмора працювала 21 хвилину без результату, вона довела менш ніж за дві хвилини.
Чому це важливо
Замість того щоб розписувати формулу далі, програма ділила задачу на дві менші й відкидала гілки, що вже суперечливі. Формули, недосяжні для попередньої програми, стали справою хвилин, а задачі на сотні рядків без кванторів — досяжними.
Програма бере від Девіса й Патнема правило одиничного диз'юнкта й правило для літералів лише одного знака, а третє правило замінює розщепленням: формула суперечлива тоді й лише тоді, коли суперечливі обидві її гілки. Твердження «рівномірна неперервність тягне неперервність», понад 500 рядків без кванторів, програма визнала загальнозначущим трохи більш ніж за дві хвилини. Пам'ять машини — 32 768 слів. Стаття Девіса й Патнема в Journal of the ACM сама називає три правила: вилучення одиничних диз'юнктів, правило для літералів одного знака й правило вилучення атомарних формул, за яким (A ∨ p) & (B ∨ ¬p) & R суперечлива тоді й лише тоді, коли суперечлива (A ∨ B) & R. Перевагу методу автори показували так: формулу, над якою програма Гілмора на IBM 704 працювала 21 хвилину без результату, їхнім методом розв'язали вручну за 30 хвилин. Журнальна версія 1962 року в Communications of the ACM пояснює заміну третього правила розщепленням: правило III швидко збільшує кількість і довжину диз'юнктів, а для машини з обмеженою швидкою пам'яттю це неприйнятно. Програму для IBM 704 Інституту математичних наук Нью-Йоркського університету повністю написано асемблером SAP.