Процедура Девіса — Патнема з розщепленням
У звіті Нью-Йоркського університету від 8 червня 1961 року Мартін Девіс, Джордж Логеман і Дональд Лавленд описали програму для IBM 704, що перевіряє формули методом Девіса й Патнема 1960 року, замінивши одне з його правил правилом розщеплення. Формулу, над якою програма Гілмора працювала 21 хвилину без результату, вона довела менш ніж за дві хвилини.
Чому це важливо
Замість того щоб розписувати формулу далі, програма ділила задачу на дві менші й відкидала гілки, що вже суперечливі. Формули, недосяжні для попередньої програми, стали справою хвилин, а задачі на сотні рядків без кванторів — досяжними.
Програма бере від Девіса й Патнема правило одиничного диз'юнкта й правило для літералів лише одного знака, а третє правило замінює розщепленням: формула суперечлива тоді й лише тоді, коли суперечливі обидві її гілки. Твердження «рівномірна неперервність тягне неперервність», понад 500 рядків без кванторів, програма визнала загальнозначущим трохи більш ніж за дві хвилини. Пам'ять машини — 32 768 слів. Чого запис не стверджує: змісту самої статті Девіса й Патнема 1960 року й журнальної версії 1962 року — обидві за платним доступом ACM; правила Девіса й Патнема тут переказано за звітом 1961 року.