Средства разработки приложений
Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов
Первый шаг. Приводим исходную формулу к предваренной нормальной форме. Для этого:
- пользуясь эквивалентностью A → B ≡ ¬A ∨ B исключим импликацию;
- перенесем все отрицания внутрь формулы, чтобы они стояли только перед атомными формулами, используя следующие эквивалентности: ¬(A ∨ B) ≡ ¬A ∧ ¬B ¬(A ∧ B) ≡ ¬A ∨ ¬B ¬(∃xA) ≡ ∀x¬A ¬(∀xA) ≡ ∃x¬A ¬¬A ≡ A
- переименовываем связанные переменные так, чтобы ни одна переменная не входила в нашу формулу одновременно связанно и свободно.
- выносим кванторы в начало формулы, используя эквивалентности:
QxA(x) ∨ B ≡ Qx(A(x) ∨ B), если B не содержит переменной x, а Q ∈ {∀, ∃}
QxA(x) ∧ B ≡ Qx(A(x) ∧ B), если B не содержит переменной x, а Q ∈ {∀, ∃}
∀xA(x) ∧ ∀xB(x) ≡ ∀x(A(x) ∧ B(x)) ∃xA(x) ∨ ∃xB(x) ≡ ∃x(A(x) ∨ B(x))Q1xA(x) ∨ Q2xB ≡ Q1xQ2y(A(x) ∨ B(y)), где Q ∈ {∀, ∃}
Q1xA(x) ∧ Q2xB ≡ Q1xQ2y(A(x) ∧ B(y)), где Q ∈ {∀, ∃}
Второй шаг. Проведем сколемизацию, т.е. элиминируем в формуле кванторы существования. Для этого для каждого квантора существования выполним следующий алгоритм.
Если устраняемый квантор существования — самый левый квантор в префиксе формулы, заменим все вхождения в формулу переменной, связанной этим квантором, на новую константу и вычеркнем квантор из префикса формулы.
Если левее этого квантора существования имеются кванторы всеобщности, заменим все вхождения в формулу переменной, связанной этим квантором, на новый функциональный символ от переменных, которые связаны левее стоящими кванторами всеобщности, и вычеркнем квантор из префикса формулы.
Проведя этот процесс для всех кванторов существования, получим формулу, находящуюся в сколемовской нормальной форме. Алгоритм устранения кванторов существования придумал Сколем в 1927 году.
Имеет место теорема о том, что формула и ее сколемизация эквивалентны в смысле выполнимости.
Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий