5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем (В.А. Захаров - Лекции)
Описание файла
Файл "5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаров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 . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,(L∃)?T1 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∀y χ(y ), ∆ i,L0 = {c 0 , c 00 }L1 = {c 0 , c 00 , c1 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3).
С каждой таблицей T ассоциирован списокиспользованных констант LT . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,(L∃)?T1 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∀y χ(y ), ∆ i,L0 = {c 0 , c 00 }L1 = {c 0 , c 00 , c1 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3). С каждой таблицей T ассоциирован списокиспользованных констант LT . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,(L∃)L0 = {c 0 , c 00 }?L1 = {c 0 , c 00 , c1 }?L2 = {c 0 , c 00 , c1 , c2 }T1 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∀y χ(y ), ∆ i,(R∀)T2 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∆, χ(c2 ) i,ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3).
С каждой таблицей T ассоциирован списокиспользованных констант LT . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,(L∃)L0 = {c 0 , c 00 }?L1 = {c 0 , c 00 , c1 }?L2 = {c 0 , c 00 , c1 , c2 }T1 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∀y χ(y ), ∆ i,(R∀)T2 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∆, χ(c2 ) i,ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3).
С каждой таблицей T ассоциирован списокиспользованных констант LT . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,(L∃)?L1 = {c 0 , c 00 , c1 }?L2 = {c 0 , c 00 , c1 , c2 }T1 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∀y χ(y ), ∆ i,(R∀)T2 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∆, χ(c2 ) i,PP(L →)PP)qPT3 = h Γ, ϕ(c1 ), ψ2 | ∆, χ(c2 ) iL3 = {c 0 , c 00 , c1 , c2 }L0 = {c 0 , c 00 }T4 = hΓ, ϕ(c1 ) | ∆, χ(c2 ), ψ1 iL4 = {c 0 , c 00 , c1 , c2 }ПОЛНОТА ТАБЛИЧНОГО ВЫВОДА3). С каждой таблицей T ассоциирован списокиспользованных констант LT . Вначале в этот списоквключаются все константы, содержащиеся в таблице T0 .В случае применения правил (L∃) и (R∀) в списокпорожденной таблицы добавляется «свежая константа».В остальных случаях список наследуется без изменений.T0 = h ∃xϕ(x), ψ1 → ψ2 , Γ | ∀y χ(y ), ∆ i,(L∃)L0 = {c 0 , c 00 }?L1 = {c 0 , c 00 , c1 }?L2 = {c 0 , c 00 , c1 , c2 }T1 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∀y χ(y ), ∆ i,(R∀)T2 = h ψ1 → ψ2 , Γ, ϕ(c1 ) | ∆, χ(c2 ) i,PP(L →)PP)qPT3 = h Γ, ϕ(c1 ), ψ2 | ∆, χ(c2 ) iT4 = hΓ, ϕ(c1 ) | ∆, χ(c2 ), ψ1 iL3 = {c 0 , c 00 , c1 , c2 }L4 = {c 0 , c 00 , c1 , c2 }и.