Алгоритм машинного поиска естественного логического вывода в исчислении высказываний / 
Н. А. Шанин, Г. В. Давыдов, С. Ю. Маслов и др. ; Акад. наук СССР. Матем. ин-т им. В. А. Стеклова. Ленингр. отд-ние. 
 - Ленинград :   Наука. [Ленингр. отд-ние] ,  1965. 
<br/><br/><label>Universal Decimal Class. No.: </label>518.5+164