12.2.5. Гиперрезолюция
Можно сделать так, чтобы в резолюции участвовали сразу по несколько предложений. Это называется гиперрезолюцией. Предположим, что для конечного множества предложений 
и единственного предложения В удовлетворяются следующие условия:
(i) В содержит 
литералов 
.
(ii) Для каждого 
предложение 
содержит литерал 
но не содержит дополнений никакого другого литерала из В и никакого литерала из любого предложения 
Множество 
будем называть конфликтом, а предложение
— его гипер резольвентой; 
можно вывести из 
В большинстве случаев к конфликту приходят только после подходящих подстановок. Иными словами, для заданного множества предложений 
не удовлетворяющего определению конфликта, может найтись такая подстановка 
, что 
будет конфликтом. В этом случае 
называется скрытым конфликтом. Поскольку обычно в резолюции одновременно участвуют только два предложения, то она — частный случай гиперрезолюции, и, таким образом, если пустое предложение 
выводится из 
при помощи резолюции, то оно также может выводиться из 
(возможно, даже быстрее) при помощи гиперрезолюции.
В качестве примера гиперрезолюции рассмотрим множество
Подстановка 
дает множество 
конфликт с резольвентой
и потому 
— скрытый конфликт.
Гиперрезолюция является примером семантической стратегии. Это объясняется тем, что конфликт 
может быть выполнимым для модели, содержащей только некоторые литералы, а именно хотя бы по одному литералу из каждого предложения конфликта, присутствующему в резольвенте конфликта. Таким образом, резольвента конфликта указывает путь, по которому можно исключить все модели.
