Математическая логика и теория алгоритмов. Стенюшкина В.А. - 40 стр.

UptoLike

ВУЗ: 

ОГУ | Оренбург

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

Рубрика: 

15 Автоматическое доказательство теорем
15.1 Постановка задачи
Алгоритм, проверяющий отношение
Г

T
S, (15.1)
называется автоматическим доказательством теорем (АДТ). Здесь
Γ - множест-
во посылок, S – заключение (формулы); T-формальная теория,
 - знак выво-
димости В общем случае такого алгоритма не существует, то есть не существу-
ет алгоритма, который для любых S, Г, T выдавал бы ответ «Да», если выводи-
мость (15.1) имеет место, и ответ «Нет», в противном случае. В некоторых слу-
чаях подобные алгоритмы существуют. Например, в случае исчисления выска-
зываний. Поскольку в ИВ теоремами являются общезначимые формулы (и то-
лько они), то для проверки выводимости достаточно построить таблицы истин-
ности.
Частичным алгоритмом АДТ (из наиболее известных) является метод ре-
золюций (МР). Для любого прикладного ИП первого порядка МР дает ответ
«Да», если (15.1) имеет место, и дает ответ «Нет» или не дает никакого ответа
(«зависает»), в противном случае. (Напомним, прикладное ИП есть ИП, которое
содержит предметные константы и
или функторы, иили предикаты и связы-
вающие их собственные аксиомы. ИП, не содержащее предметных констант,
функторов, предикатов и собственных аксиом, называется чистым.)
15.2 Основа метода резолюций
Теорема Если Г, S  F, где F – тождественно ложная формула (проти-
воречие), то Г
 S.
Эта теорема лежит в основе МР, то есть используется идея «доказательс-
тва от противного».
В качестве противоречия принято использовать так называемую «пус-
тую» формулу и обозначать «пустым» квадратом:
.
15.3 Правило резолюции
Метод резолюций работает с предложениями. Напомним, предложение –
бескванторная дизъюнкция литералов, а литералы – это формулы вида А,
А,
где А – атом. Далее будет показана методика перехода от формулы ИП к мно-
жеству предложений.
Правило резолюции для ИВ: пусть С
1
, С
2
– предложения в ИВ, причем С
1
= Р
∨С
1
′, С
2
= Р ∨С
2
′, где Р – пропозициональная переменная, С
1
′, С
2
′ - пред- 
      15 Автоматическое доказательство теорем

      15.1 Постановка задачи

     Алгоритм, проверяющий отношение

                                   Г T S,                              (15.1)

называется автоматическим доказательством теорем (АДТ). Здесь Γ - множест-
во посылок, S – заключение (формулы); T-формальная теория,  - знак выво-
димости В общем случае такого алгоритма не существует, то есть не существу-
ет алгоритма, который для любых S, Г, T выдавал бы ответ «Да», если выводи-
мость (15.1) имеет место, и ответ «Нет», в противном случае. В некоторых слу-
чаях подобные алгоритмы существуют. Например, в случае исчисления выска-
зываний. Поскольку в ИВ теоремами являются общезначимые формулы (и то-
лько они), то для проверки выводимости достаточно построить таблицы истин-
ности.
      Частичным алгоритмом АДТ (из наиболее известных) является метод ре-
золюций (МР). Для любого прикладного ИП первого порядка МР дает ответ
«Да», если (15.1) имеет место, и дает ответ «Нет» или не дает никакого ответа
(«зависает»), в противном случае. (Напомним, прикладное ИП есть ИП, которое
содержит предметные константы и или функторы, иили предикаты и связы-
вающие их собственные аксиомы. ИП, не содержащее предметных констант,
функторов, предикатов и собственных аксиом, называется чистым.)

      15.2 Основа метода резолюций

      Теорема Если Г,  S  F, где F – тождественно ложная формула (проти-
воречие), то Г S.
      Эта теорема лежит в основе МР, то есть используется идея «доказательс-
тва от противного».
      В качестве противоречия принято использовать так называемую «пус-
тую» формулу и обозначать «пустым» квадратом: .

      15.3 Правило резолюции

     Метод резолюций работает с предложениями. Напомним, предложение –
бескванторная дизъюнкция литералов, а литералы – это формулы вида А,  А,
где А – атом. Далее будет показана методика перехода от формулы ИП к мно-
жеству предложений.
     Правило резолюции для ИВ: пусть С1, С2 – предложения в ИВ, причем С1
= Р ∨С1′, С2 =  Р ∨С2′, где Р – пропозициональная переменная, С1′, С2′ - пред-

Страницы