Математическая логика и теория алгоритмов

Таким образом, применяя правило резолюции к дизъюнктам (1) и (2) по iP и з1 Р получаем следующий дизъюнкт: (?)2qv,q. Литера 2Q и 4Q одна и та же. Так как 2<4, то Q получает индекс 2, поэтому получаем (4) 2 0 . Дизъюнкт (4) и является лок-резолъвентой дизъюнктов (1) и (2). Отметим, что если бы литеры в дизъюнкте (2) были индексиро­ ваны иначе, например, так: (2')4lPv3e, то литерой в дизъюнкте (2*), которую разрешено отрезать, была бы 30. Однако к iP и зб нельзя применить правило резолюции. Поэтому не существует лок-резольвенты дизъюнктов (1) и (2*). Под лок-резолю'цией понимается последовательное получение лок-резольвент из данного множества дизъюнктов и вновь получае­ мых дизъюнктов. Рассмотрим множество S дизъюнктов, которое введено в § 4: p^q. p v i e . 1Pv 1б . Проведем следующую индексацию: (1) i/'v (2)зРУ41б, (3)61PV5S (4) s IPvv l e . Из дизъюнктов (1)-(4) можно получить только одну лок-резольвенту (5)б1Р из(3)и(4), а из дизъюнктов (1) - (5) только две лок-резольвенты: (6)26 из(1)и(5), { 1 ) ^ Q из (2) и (5). 9 9