Лекции В.А. Захарова (1157993), страница 6
Текст из файла (страница 6)
. . , dn i çíà÷åíèéñâîáîäíûõ ïåðåìåííûõ, äëÿ êîòîðûõ I |= Γ[d̄],I 6|= ∆[d̄],I |= (ϕ → ψ)[d̄]⇐⇒ I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄]⇐⇒èëè I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄] èëè I 6|= ϕ[d̄] I |= Γ[d̄],I 6|= ∆[d̄],I 6|= ϕ[d̄]⇐⇒⇐⇒îäíà èç òàáëèö T1 = hΓ, ψ|∆i èëè T2 = hΓ|ϕ, ∆i âûïîëíèìà.ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììûÀíàëîãè÷íî äîêàçûâàåòñÿ êîððåêòíîñòü îñòàëüíûõ 7 ïðàâèëäëÿ ëîãè÷åñêèõ ñâÿçîêÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû∀x0 ϕ(x0 )|∆i.Ðàññìîòðèì ïðàâèëî L∀: hΓ, ∀x0hΓ,ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iÒàáëèöà hΓ, ∀x0ϕ(x0)|∆i âûïîëíèìà ⇐⇒ ñóùåñòâóåòèíòåðïðåòàöèÿ I è íàáîð d1, . .
. , dn çíà÷åíèé ñâîáîäíûõïåðåìåííûõ, äëÿ êîòîðûõ I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],I |= (∀x0 ϕ)[d1 , . . . , dn ]Ïóñòü d0 = t[d1, . . . , dn ]. ÒîãäàI |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒.Ñëåäîâàòåëüíî, òàáëèöàâûïîëíèìà â èíòåðïðåòàöèè .Íà êàêîì ýòàïå äîêàçàòåëüñòâà ñóùåñòâåííî èñïîëüçóåòñÿ òîòôàêò, ÷òî ïåðåìåííàÿ x0 ñâîáîäíà äëÿ òåðìà t â ôîðìóëå ϕ ?⇒ I |= ϕ[t[d1 , . . .
, dn ], d1 , . . . , dn ] ⇒ I |= ϕ{x0 /t}[d1 , . . . , dn ]hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iIÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû∃xϕ(x)|∆i.Ðàññìîòðèì ïðàâèëî L∃: hΓ,hΓ,ϕ(x){x/c}|∆iÎ÷åâèäíî, ÷òî âûïîëíèìîñòü òàáëèöû hΓ, ϕ(x){x/c}|∆i âëå÷åòâûïîëíèìîñòü òàáëèöû hΓ, ∃xϕ(x)|∆iÄîïóñòèì, ÷òî âûïîëíèìà òàáëèöà hΓ, ∃xϕ(x)|∆i. Òîãäàñóùåñòâóåò èíòåðïðåòàöèÿ I è íàáîð d1, . . .
, dn çíà÷åíèéñâîáîäíûõ ïåðåìåííûõ, äëÿ êîòîðûõ I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],I |= (∃xϕ)[d1 , . . . , dn ]Âûïîëíèìîñòü ∃xϕ[d1, . . . , dn ] îçíà÷àåò, ÷òî ñóùåñòâóåò òàêîéýëåìåíò d0 ∈ DI , ÷òî I |= ϕ[d0, d1, . . . , dn ].ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììûÐàññìîòðèì èíòåðïðåòàöèþ J , êîòîðàÿ îòëè÷àåòñÿ îò I , òîëüêîòåì, ÷òî â J êîíñòàíòà c èìååò äðóãîå çíà÷åíèå, à èìåííîc̄ = d0 .Òîãäà J |= (ϕ{x/c})[d1, .
. . , dn ].Êðîìå òîãî, J |= Γ[d1, . . . , dn ] è J 6|= ∆[d1, . . . , dn ].Ñëåäîâàòåëüíî, òàáëèöà hΓ, ϕ(x){x/c}|∆i âûïîëíèìà âèíòåðïðåòàöèè J .Íà êàêîì ýòàïå äîêàçàòåëüñòâà ñóùåñòâåííî èñïîëüçóåòñÿ òîòôàêò, ÷òî êîíñòàíòà c íå âõîäèò â ñîñòàâ ôîðìóë èç Γ, ∆ èôîðìóëû ϕ ?ÊÎÐÐÅÊÒÍÎÑÒÜ ÒÀÁËÈ×ÍÎÃÎ ÂÛÂÎÄÀÒåîðåìà êîððåêòíîñòè òàáëè÷íîãî âûâîäàÅñëè äëÿ ñåìàíòè÷åñêîé òàáëèöû T0 ñóùåñòâóåòóñïåøíûé òàáëè÷íûé âûâîä, òî òàáëèöà T0íåâûïîëíèìà.ÄîêàçàòåëüñòâîÑëåäóåò èçI îïðåäåëåíèÿ òàáëè÷íîãî âûâîäà,I ëåììû î êîððåêòíîñòè ïðàâèë òàáëè÷íîãî âûâîäà,I è óòâåðæäåíèÿ î íåâûïîëíèìîñòè çàêðûòûõ òàáëèö.ÑëåäñòâèåÅñëè äëÿ òàáëèöû Tϕ = h ∅ |ϕ i ìîæíî ïîñòðîèòü óñïåøíûéòàáëè÷íûé âûâîä, òî |= ϕ.ÊÎÍÅÖ ËÅÊÖÈÈ 4.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаровzakh@cs.msu.suhttp://mathcyb.cs.msu.su/courses/logprog.htmlЛекция 5.Полнота табличного вывода.Теорема Левенгейма-Сколема.Теорема компактности Мальцева.Автоматическое доказательствотеорем.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДАТеорема полноты табличного выводаЕсли семантическая таблица T0 невыполнима, то для T0существует успешный табличный вывод.Доказательство.Проведем для упрощенного частного случая таблицы T0 , вкоторойIимеется лишь конечное число формул,Iвсе формулы замкнутые,Iв формулах нет функциональных символов.Пусть T0 = h Γ0 | ∆0 i — невыполнимая таблица.
Будемстроить табличный вывод для T0 , руководствуясь следующейстратегией.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.yT0ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty1yT0@@@R yT@2ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.yT0@@@R yT@2Ty3Ty1@@@R yT@4ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1).
Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty3yT0@@@R yT@Ty12@@@@@@R yT@R yT@4закр. табл.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1). Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty3yT0@@@R yT@Ty12@@@@@@R yT@R yT@4закр. табл.?yTзакр. табл.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА1).
Каждая незакрытая таблица в дереве вывода получаетпорядковый номер, и правила табличного выводаприменяются к таблицам в порядке возрастания ихномеров.Ty3yT0@@@R yT@Ty12@@@@@@R yT@R yT@4закр. табл.?yTзакр. табл.?yT5и. т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках.
Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ iПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ iПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ i(L∀)?T1 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | χ1 ∨ χ2 , ∆ iПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2).
Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ i(L∀)?T1 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | χ1 ∨ χ2 , ∆ iПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ i(L∀)?T1 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | χ1 ∨ χ2 , ∆ i(R∨)?T2 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | ∆, χ1 , χ2 iПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2).
Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ i(L∀)?T1 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | χ1 ∨ χ2 , ∆ i(R∨)?T2 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | ∆, χ1 , χ2 iПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков).
Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ i(L∀)?T1 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | χ1 ∨ χ2 , ∆ i(R∨)?T2 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | ∆, χ1 , χ2 iPPPP(L →))PqT3 = h Γ, ∀xϕ, ϕ0 , ψ2 | ∆, χ1 , χ2 i T4 = hΓ, ∀xϕ, ϕ0 | ∆, χ1 , χ2 , ψ1 iПОЛНОТА ТАБЛИЧНОГО ВЫВОДА2). Таблицы состоят из упорядоченных множеств формул(списков). Правила применяются к формулам в порядке ихрасположения в списках. Формулы, участвующие вприменении правил, помещаются в хвост нужного списка.Атомарные формулы просто переходят из головы списка вего хвост.T0 = h ∀xϕ, ψ1 → ψ2 , Γ | χ1 ∨ χ2 , ∆ i(L∀)?T1 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | χ1 ∨ χ2 , ∆ i(R∨)?T2 = h ψ1 → ψ2 , Γ, ∀xϕ, ϕ0 | ∆, χ1 , χ2 iPP(L →)PP)PqT3 = h Γ, ∀xϕ, ϕ0 , ψ2 | ∆, χ1 , χ2 i T4 = hΓ, ∀xϕ, ϕ0 | ∆, χ1 , χ2 , ψ1 iи.
т. д.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3). С каждой таблицей T ассоциирован списокиспользованных констант LT . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3). С каждой таблицей T ассоциирован списокиспользованных констант LT .
Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,L0 = {c 0 , c 00 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3). С каждой таблицей T ассоциирован списокиспользованных констант LT . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,L0 = {c 0 , c 00 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3). С каждой таблицей T ассоциирован списокиспользованных констант LT .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
