Средства разработки приложений
В частности, он предложил вместо
В частности, он предложил вместо правила вывода «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.
Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий