5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем (1158020)
Текст из файла
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаров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 }и.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
