Новиков Ф.А. Дискретная математика для программистов (860615), страница 33
Текст из файла (страница 33)
При этом вполнеможет статься, что непротиворечивость одной конкретной теории может быть установлена средствами другой, более мощной формальной теории. Но тогда возникает вопрос онепротиворечивости этой второй теории и т. д.4.5. Автоматическое доказательство теоремАвтоматическое доказательство теорем — это краеугольный камень логическогопрограммирования, искусственного интеллекта и других современных направлений в программировании.
Здесь излагаются основы метода резолюций — классического (и в то же время до сих пор популярного) метода автоматическогодоказательства теорем, предложенного Робинсоном1 в 1965 году.4.5.1. Постановка задачиАлгоритм, который проверяет отношениеГКг Sдля формулы S, множества формул Г и теории Т, называется алгоритмом автоматического доказательства теорем.
В общем случае такой алгоритм невозможен, то есть не существует алгоритма, который для любых S, Г и Т выдавал быответ «Да», если Г b j S, и ответ «Нет», если неверно, что Г Ь^ S. Более того, известно, что нельзя построить алгоритм автоматического доказательства теоремдаже для большинства конкретных достаточно богатых формальных теорий XВ некоторых случаях удаётся построить алгоритм автоматического доказательства теорем, который применим не ко всем формулам теории (то есть частичныйалгоритм, см. 4.2.5).Для некоторых простых формальных теорий (например, для исчисления высказываний) и некоторых простых классов формул (например, для прикладногоисчисления предикатов с одним одноместным предикатом) алгоритмы автоматического доказательства теорем известны.1Джон А. Робинсон (р.
1930).172Глава 4. Логические исчисленияПример Поскольку для исчисления высказываний известно, что теоремамиявляются общезначимые формулы, можно воспользоваться простым методомпроверки общезначимости формулы с помощью таблиц истинности. А именно,достаточно вычислить истинностное значение формулы при всех возможных интерпретациях (их конечное число). Если во всех случаях получится значениеТ, то проверяемая формула — тавтология и, следовательно, является теоремойтеорииЕсли же хотя бы в одном случае получится значение F, то проверяемая формула не является тавтологией и, следовательно, пе является теоремойтеорииЗАМЕЧАНИЕПриведённый выше пример является алгоритмом автоматического доказательства теоремв теории £, хотя и пе является алгоритмом автоматического поиска вывода теорем изаксиом теории L.Наиболее известный классический алгоритм автоматического доказательства теорем называется методом резолюций.
Для любого прикладного исчисления предикатов первого порядка Т, любой формулы S и множества формул Г теории Тметод резолюций выдаёт ответ «Да», если Г Ь^- S, и выдаёт ответ «Нет» или певыдаёт никакого ответа (то есть «зацикливается»), если неверно, что Г Ь-j S.4.5.2. Доказательство от противногоВ основе метода резолюций лежит идея «доказательства от противного».Если Г, ->5 Ь F, где F — любое противоречие (тождественно ложнаяформула), то Г I- S.ТЕОРЕМАДОКАЗАТЕЛЬСТВОГ & ->S(ДЛЯслучая £ ) Г,I- FГ &; ->S —> F — тавтология.
НоF = - ( Г к -nS) V F = -i(r к -iS)Имеем: Г —> S — тавтологияГ I- S.=-ГV5 = Г -> S.•Пустая формула не имеет никакого значения ни в какой интерпретации, в частности, пе является истинной ни в какой интерпретации и, по определению, является противоречием. В качестве формулы F при доказательстве от противногопо методу резолюций принято использовать пустую формулу. Полезно сравнитьиспользование пустой формулы в методе резолюций с подразделом 3.4.2.ЗАМЕЧАНИЕПри изложении метода резолюций пустая формула традиционно обозначается • . Однакозначок • занят в книге для обозначения конца доказательства, поэтому для обозначенияпустой формулы в этом разделе мы используем нетрадиционный знак •1734.5. Автоматическое доказательство теорем4.5.3. Сведение к предложениямМетод резолюций работает с особой стандартной формой формул, которые называются предложениями.
Предложение — это бескванторная дизъюнкция литералов. Любая формула исчисления п р е д и к а т о в может быть преобразована вмножество предложений следующим образом (здесь знак н-> используется дляобозначения способа преобразования формул):1. Элиминация импликации.
Преобразование:А->В •-> n i vВ.После первого этапа формула содержит толькоV, & , V, 3.2. Протаскивание отрицаний. Преобразования:-Д/х (-4) |-> З х (~>А),->3х (Л)V x (->Л),->(А V Б ) Н-> - > Л & - П Б ,^(А & В ) Н . Л V ->В.н-> А,После второго этапа формула содержит отрицания только перед атомами.3.
Разделение связанных переменных. Преобразование:QixA(...Q2XB(...X...)...)^Q i x A{...Q2yВ{...у...)...),где Q\ и Q2 — любые кванторы. После третьего этапа формула не содержитслучайно совпадающих связанных переменных.4. Приведение к предварённой форме. Преобразования:Qx АVВ ^ Qx {АVВ),Qx А & В ^ Qx{А & В),где Q — любой квантор. После четвёртого этапа формула находится в предварённой форме.5. Элиминация кванторов существования (сколемизация). Преобразования:3 X I (Q2X-2 ...QnxnA ( X I , X 2 , . .
. , Х П ) ) Н^ Q2x2 .. .QnxnЛ(А, Х 2 , . . . , XN),V x i (... V x i _ i (3 xi (Qi+lxi+1...Qnxn^(xi,...,xi,...,xn)))...)i-^ V x i ( . . . V x i _ i (Qi+i xi+i ... QnxnA(x1,..., / ( x i , . . . ,Xi_i),... ,xn))...),где a — новая предметная константа, / — новый функциональный символ,a Q1,Q2,...,Qn— любые кванторы. После пятого этапа формула содержиттолько кванторы всеобщности.6. Элиминация кванторов всеобщности.
Преобразование:V x (Л(х))А{х).После шестого этапа формула не содержит кванторов.7. Приведение к конъюнктивной нормальной форме. Преобразования:АV(В & С) ^ [АVВ)&(АVС),{А & В)VС^(АVС) & (ВVС).После седьмого этапа формула находится в конъюнктивной нормальной форме.8. Элиминация конъюнкции. Преобразование:А К ВИА,В.После восьмого этапа формула распадается на множество предложений.Не все преобразования на этапах 1 - 8 являются логически эквивалентными.174Глава 4. Логические исчисленияТЕОРЕМА Если Г — множество предложений, полученных из формулы S, то Sявляется противоречием тогда и только тогда, когда множество Г невыполнимо.В доказательстве нуждается шаг 5 — сколемизация.
Пусть1 (. ..V®<_ i (3xiQi+ixi+i...Qnxn (A(xi,..., x n ) ) ) . . . ) . ПоложимДОКАЗАТЕЛЬСТВОF:=VxF': = V x i (... Vxi-i(Qi+iXi+i...Xi-i,QnxnA(x\,...,/ ( z i , . . . , Xi-i), £ i + i , . . . ,xn)...)).Пусть F — противоречие, a f - не противоречие. Тогда существуют интерпретация I и набор значений s — ( a i , . . .
, Oj_i, a*+i,..., an), такие, что s*(F') = Т.Положим ai: = / ( a i , . . . ,a»_i), si : = ( a i , . . . , a . _ i , a i , a i + i , . . . , a n ) . Тогда sJ(F) = T,и F — выполнимая формула.•ЗАМЕЧАНИЕНевыполнимость множества формул Г означает, что множество Г не имеет модели, то естьне существует интерпретации, в которой все формулы Г имели бы значение Т.4.5.4. Правило резолюции для исчислениявысказыванийМетод резолюций основан на использовании специального правила вывода.Пусть Сi и С2 — два предложения в исчислении высказываний и пустьС\ = Р V С[, а С2 = -1Р V С'2, где Р — пропозициональная переменная, а С[, С'2 —любые предложения (в частности, может быть, пустые или состоящие только изодного литерала). Правило выводаС ь С2(,называется правилом резолюции. Предложения С\ и С2 называются резольвируемыми (или родительскими), предложение С[ V С'2 — резольвентой, а формулыР и -лР — контрарными литералами.ЗАМЕЧАНИЕРезольвента является предложением, то есть множество предложений замкнуто относительно правила резолюции.1 Правило резолюции логично, то есть резольвента является логическим следствием резольвируемых предложений.ТЕОРЕМАПусть I(C\) = Т и /(Сг) = Т.
Тогда если I(P) = Т, то С'2 Ф 0и 1{С'2) = Т, а значит, 1{С[ V С'2) = Т. Если же 1{Р) = ¥,тоС[ф0и1{С[) = Т,а значит, I(C[ V С^) = Т.•ДОКАЗАТЕЛЬСТВО1754.5. Автоматическое доказательство теоремПравило резолюции — это очень мощное правило вывода. Многие ранее рассмотренные правила являются его частными случаями:А,А-+В..—ВЛ ^ В, В ^С—А->С,Modus ponensДпА v В „R,в-пЛ V В, ->В V С „—R,пЛ V С^ТраизитивиостьА V В,А ^ В ^СлияниеВЛ VP,VPВR.Правило резолюции полно, то есть всякая тавтология может бытьвыведена с использованием только правила резолюции.ТЕОРЕМА 2ДОКАЗАТЕЛЬСТВОБез доказательства.•4.5.5. Правило резолюции для исчисления предикатовДля применения правила резолюции нужны контрарные литералы в резольвируемых предложениях. В случае исчисления высказываний контрарные литералыопределяются очень просто: это пропозициональная переменная и её отрицание.Для исчисления предикатов определение чуть сложнее.Пусть С\ и С2 — два предложения в исчислении предикатов.
Правило выводаС*' С 2(р\(С[ V С'2)аназывается правилом резолюции в исчислении предикатов, если в предложенияхС\ и Сг существуют унифицируемые контрарные литералы Pi и Р2, то есть С\ == Pi V С[ и С2 = ->Р2 V С'2, причём атомарные формулы Pi иунифицируютсянаиболее общим унификатором и. В этом случае резольвентой предложений С\и С2 является предложение (С{ V С'2)а, полученное из предложения С[ V С2применением унификатора а.4.5.6. Опровержение методом резолюцийОпровержение методом резолюций — это алгоритм автоматического доказательства теорем в прикладном исчислении предикатов, который сводится к следующему.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
