Составители:
Рубрика:
28
Тогда С
2
σ = С
`
2
= ¬ P(f(y)) ∨ Q(y) и резольвентой для С
1
и С
`
2
будет С =
¬
R(b) ∨ Q(y).
Принцип резолюции обладает важным свойством – полнотой,
которое устанавливается следующей теоремой (Дж. Робинсон):
Множество дизъюнктов S невыполнимо тогда и только тогда,
когда существует вывод из S пустого дизъюнкта.
Однако в силу неразрешимости логики предикатов первого
порядка для выполнимого множества дизъюнктов S процедура,
основанная на принципе резолюции, будет работать бесконечно
долго.
Приведем два примера,
иллюстрирующих принцип резолюции для
логики предикатов.
Пример.
Существуют студенты, которые любят всех
преподавателей. Ни один из студентов не любит невежд.
Следовательно, ни один из преподавателей не является невеждой.
Запишем эти утверждения на языке логики предикатов и
приведем их к стандартному виду:
∃ x (С(х) &
∀
y (P(y) → L(х, y))),
∀ x (С(х) →
∀
y (H(y) → L(х, y))),
∀ y(P(y) →
¬
H(y)).
1. С(a).
2.
¬ P(y) ∨ L(a, y).
3.
¬ С(х) ∨ ¬ H(y) ∨ ¬ L(х, y).
¬
∀ y(
¬
P(y) ∨
¬
H(y))= ∃ y(P(y) &H(y)).
4. P(b).
5. H(b).
6. L(a, b) (2, 4). σ = {b/y}.
7.
¬ H(y)
∨
¬ L(a, y) (1, 3). σ = {b/x}.
8.
¬ L(a, b) (6, 7). σ = {b/y}.
9. (6,8).
Принцип резолюции является более эффективной процедурой
вывода, нежели процедура Эрбрана. Но и он имеет существенный
недостаток, заключающийся в формировании всевозможных
резольвент, большинство из которых оказываются излишними и
поэтому ненужными. С 1965 года и по сей день появляются
всевозможные модификации принципа резолюции, направленные на
нахождение более эффективных стратегий поиска
нужных
дизъюнктов.
Тогда С 2 σ = С ` 2 = ¬ P(f(y)) ∨ Q(y) и резольвентой для С 1 и С ` 2
будет С = ¬ R(b) ∨ Q(y).
Принцип резолюции обладает важным свойством – полнотой,
которое устанавливается следующей теоремой (Дж. Робинсон):
Множество дизъюнктов S невыполнимо тогда и только тогда,
когда существует вывод из S пустого дизъюнкта.
Однако в силу неразрешимости логики предикатов первого
порядка для выполнимого множества дизъюнктов S процедура,
основанная на принципе резолюции, будет работать бесконечно
долго.
Приведем два примера, иллюстрирующих принцип резолюции для
логики предикатов.
Пример. Существуют студенты, которые любят всех
преподавателей. Ни один из студентов не любит невежд.
Следовательно, ни один из преподавателей не является невеждой.
Запишем эти утверждения на языке логики предикатов и
приведем их к стандартному виду:
∃ x (С(х) & ∀ y (P(y) → L(х, y))),
∀ x (С(х) → ∀ y (H(y) → L(х, y))),
∀ y(P(y) → ¬ H(y)).
1. С(a).
2. ¬ P(y) ∨ L(a, y).
3. ¬ С(х) ∨ ¬ H(y) ∨ ¬ L(х, y).
¬ ∀ y( ¬ P(y) ∨ ¬ H(y))= ∃ y(P(y) &H(y)).
4. P(b).
5. H(b).
6. L(a, b) (2, 4). σ = {b/y}.
7. ¬ H(y) ∨ ¬ L(a, y) (1, 3). σ = {b/x}.
8. ¬ L(a, b) (6, 7). σ = {b/y}.
9. (6,8).
Принцип резолюции является более эффективной процедурой
вывода, нежели процедура Эрбрана. Но и он имеет существенный
недостаток, заключающийся в формировании всевозможных
резольвент, большинство из которых оказываются излишними и
поэтому ненужными. С 1965 года и по сей день появляются
всевозможные модификации принципа резолюции, направленные на
нахождение более эффективных стратегий поиска нужных
дизъюнктов.
28
