 |
| English | Russian |
| Davis-Putnam-Logemann-Loveland algorithm | алгоритм Дэвиса-Патнема-Логемана-Лавленда (полный алгоритм поиска с возвратом для определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме. Опубликован в 1962 г. Мартином Дэвисом, Хилари Патнемом, Джорджем Логеманом и Дональдом Лавлендом, представляет собой усовершенствование более раннего алгоритма Дэвиса-Патнема (1960 г.), основанного на правиле резолюций Alex_Odeychuk) |