Логическое программирование на языке Visual Prolog. Солдатова О.П - 11 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

11
{
¬
P(x, f(x))
∨
R(x, f(x), g(x)), Q(x, g(x))
∨
R(x, f(x), g(x)),
¬
Q(x, g(x))
∧
P(x,
f(x))}.
Теорема 1. Пусть S – множество дизъюнктов, которые
представляют ССФ формулы F. Тогда F противоречива в том и только в
том случае, когда S противоречиво.
Теорема 2. Пусть даны формулы F
1
, F
2
,…, F
n
и формула G. G есть
логическое следствие F
1
, F
2
,…, F
n
тогда и только тогда, когда формула ((F
1
∧
F
2
∧
…
∧
F
n
)
→
G) общезначима.
Теорема 3. Пусть даны формулы F
1
, F
2
,…, F
n
и формула G. G есть
логическое следствие F
1
, F
2
,…, F
n
тогда и только тогда, когда формула (F
1
∧
F
2
∧
…
∧
F
n
∧¬
G) противоречива.
Замечание.
Для того чтобы доказать, что данная формула является
тавтологией, достаточно доказать, что ее отрицание является
противоречием:
¬
((F
1
∧
F
2
∧
…
∧
F
n
)
→
G)=
¬
(
¬
(F
1
∧
F
2
∧
…
∧
F
n
)
∨
G)=
(F
1
∧
F
2
∧
…
∧
F
n
)
∧
¬
G).
На основании теорем 1 и 3 можно сделать вывод, что формула G
является логическим следствием формулы F тогда, когда противоречива
конъюнкция множества S и формулы
¬
G, то есть противоречива формула
S
1
∧
S
2
∧
…S
n
∧
¬
G. Таким образом, если в множество S добавить
негативный литерал
¬
G и доказать, что полученное множество
противоречиво, то тем самым можно доказать выводимость G из
множества S.
1.2.3 Метод резолюций в исчислении высказываний.
Основная идея метода резолюций состоит в том, чтобы проверить,
содержит ли множество дизъюнктов пустой дизъюнкт. Если множество
содержит пустой дизъюнкт, то оно противоречиво (невыполнимо). Если
множество не содержит пустой дизъюнкт, то
проверяется следующий факт:
может ли пустой дизъюнкт быть получен из данного множества. Множество
содержит пустой дизъюнкт, тогда и только тогда, когда оно пустое. Если
множество можно свести к пустому, то тем самым можно доказать его
противоречивость. В этом и состоит метод резолюций, который часто
рассматривают как специальное правило вывода, используемое
для
порождения новых дизъюнктов из данного множества.
Определение 3:Если A атом, то литералы A и
¬
A контрарны друг
другу, и множество { A,
¬
A } называется контрарной парой.
Отметим, что дизъюнкт есть тавтология, если он содержит
контрарную пару.
Определение 4: Правило резолюций состоит в следующем:

Страницы