Средства разработки приложений


Алгоритм унификации - часть 2


В частности, он предложил вместо правила вывода «modus ponens», которое утверждает, что из A и A > B выводится B, использовать его обобщение, правило резолюции, которое сложнее понимается человеком, но эффективно реализуется на компьютере. Давайте попробуем разобраться с этим правилом.

Правило резолюции для логики высказываний можно сформулировать следующим образом.

Если для двух дизъюнктов существует атомная формула, которая в один дизъюнкт входит положительно, а в другой отрицательно, то, вычеркнув соответственно из одного дизъюнкта положительное вхождение атомной формулы, а из другого — отрицательное, и объединив эти дизъюнкты, мы получим дизъюнкт, называемый резольвентой. Исходные дизъюнкты в таком случае называются родительскими или резольвируемыми, а вычеркнутые формулы — контрарными литералами. Другими словами, резольвента — это дизъюнкт, полученный из объединения родительских дизъюнктов вычеркиванием контрарных литералов.

Графически это правило можно изобразить так:

(A ∨B, P ∨ ¬P)/A ∨ B

Здесь A ∨ P и B ∨ ¬P — родительские дизъюнкты, P и ¬P — контрарные литералы, A ∨ B — резольвента.

Если родительские дизъюнкты состояли только из контрарных литералов, то резольвентой будет пустой дизъюнкт.

Пример. Правило вывода «modus ponens» получается из правила резолюции, если взять в качестве родительских дизъюнктов C1=A, C2=¬A ∨ B(≡ A > B). Контрарными литералами в применении этого правила будут A и ¬A, резольвентой — формула B.

Сформулируем правило резолюции для логики первого порядка.

Пусть имеется два дизъюнкта C1 и C2, у которых нет общих переменных, L1 — литерал, входящий в дизъюнкт C1, L2 — литерал, входящий в дизъюнкт C2. Если литералы имеют наибольший общий унификатор ?, то дизъюнкт (C1?–L1?)∪(C2?–L2?) называется резольвентой дизъюнктов C1 и C2. Литералы L1 и L2 называются контрарными литералами. То же правило записывается в графическом виде как

(A ∨ P2, B ∨ ¬P2)/(A ∨ B)?

Здесь P1 и P2 — контрарные литералы, (A ∨ B)? — резольвента, полученная из дизъюнкта (A ∨B) применением унификатора ?, A ∨ P1 и B ∨ P2 — родительские дизъюнкты, а ? — наибольший общий унификатор P1 и P2.




Начало  Назад  Вперед