Теормин 2014 (микро) (Мадорский) (1162045), страница 2
Текст из файла (страница 2)
(Фактически, унификатор θ = {x1/r1, …, xk/rk} — это решение системыуравнений E в свободной алгебре термов). Соответствующим образом определяется и наиболее общий унификаторсистемы уравненийОписание алгоритма унификации (Алгоритм Мартелли–Монтанари): Это — недетерминированный алгоритм,состоящий из 6 правил, которые можно применять в любом порядке до тех пор, пока: 1) либо ни одно из правилприменить невозможно (построена приведенная система уравнений), 2) либо применяется правило, устанавливающееневозможность унификации.Правило резолюции: Пусть D1 = D1’ ∨ L1 и D2 = D2’ ∨ ¬L2 — два дизъюнкта.
Пусть θ ∈ НОУ(L1, L2). Тогда дизъюнкт D0 =(D1’∨D2’)θ называется резольвентой дизъюнктов D1 и D2. Правило резолюцииD1`∨ L1,D2`∨ ¬L2,(D1`∨ D2`)θθ ∈ НОУ(L1, L2)Правило склейки: Пусть D1 = D1’ ∨ L1 ∨ L2 — дизъюнкт. Пусть η ∈ НОУ(L1, L2). Тогда дизъюнкт D0= (D1’ ∨ L1)η называетсясклейкой дизъюнкта D1.
Пара литер L1 и L2 назыв. склеиваемой парой. Правило склейкиD1`∨ L1 ∨ L2,(D1`∨ L1)ηη ∈ НОУ(L1, L2)Пусть S = {D1, D2, …, DN} — система дизъюнктов. Резолютивным выводом из системы дизъюнктов S называетсяконечная последовательность дизъюнктов D1’, D2’, …, Di’, Di+1’, …, Dn’, в которой для любого i, 1 ≤ i ≤ n, выполняетсяодно из трехусловий: 1) либо Di’ — вариант некоторого дизъюнкта из S, 2) либо Di’ — резольвента дизъюнктов Dj’ и Dk’,где j , k < i, 3) либо Di’ — склейка дизъюнкта Dj’, где j < i.Дизъюнкты D1’, D2’, …, Dn’ считаются резолютивно выводимыми из системы S.Резолютивный вывод называется успешным (или, подругому, резолютивным опровержением), если этот выводоканчивается пустым дизъюнктом □.Теорема корректности резолютивного вывода: Если из системы дизъюнктов S резолютивно выводим пустой дизъюнкт□, то S — противоречивая система дизъюнктов.
(следует из лемм, доказывающих, что склейка и резольвента являютсялогическими следствиями) Лемма 1: Если D0— резольвента дизъюнктов D1 и D2, то D1, D2|= D0Лемма 2: Если D0 — склейка дизъюнкта D, то D |= D0.Теорема о полноте резолютивного вывода: Если S – противоречивая система дизъюнктов, то из S резолютивновыводим пустой дизъюнкт □.
(По теореме Эрбрана можно свести противор. сист. дизъюнктов к конечности, потом восп.леммой об основных примерах дизъюнктов, а потом перейдём от неё к самим дизъюнктам через лемму о подъёме)Теорема полноты I–резолюции: Если система дизъюнктов S противоречива, то для любой интерпретации I существуетуспешный I-резолютивный вывод пустого дизъюнкта □ из S .Определение SLD-резолюции: Пусть: 1) G = ? C1, …, Ci, …, Cm — целевое утверждение, в котором выделена подцель Ci,2) D’= A0’← A1’, A2’, …, An’ — вариант некоторого программного утверждения, в котором VarG ∩ VarD’ = ∅, 3) θ ∈ НОУ(Ci,A0’) — наиб. общ. унификатор подцели Ci и заголовка программного утверждения A0’. Тогда запрос G’ = ?(C1, …, Ci−1, A1’,A2’, …, An’, Ci+1, …, Cm)θ называется SLD-резольвентой программного утверждения D’ и запроса G с выделеннойподцелью Ci и унификатором θ.Определение (SLD-резолютивного вычисления) Пусть: 1) G0 = ? C1, C2, …, Cm — целевое утверждение с целевымипеременными Y1, Y2, .
. . , Yk, 2) P = {D1, D2, …, DN} — хорновская логическая программа, 3) comp = (Dj1, θ1, G1), (Dj2, θ2,G2), …, (Djn, θn, □) — успешное SLD-резолютивное вычисление, порожденное запросом G к программе P.Тогда подстановка θ = (θ1 θ2 … θn)|Y1,Y2,...,Yk, представляющая собой композицию всех вычисленных унификаторов θ1,θ2, …, θn, ограниченную целевыми переменными Y1, Y2, …, Yk, называется вычисленным ответом на запрос G0 кпрограмме P.Теорема (корректности операционной семантики): Пусть: 1)G0= ? C1, C2, …, Cm — целевое утверждение, 2) P ={D1, D2, …, DN} — хорновская логическая программа, 3) θ — вычисленный ответ на запрос G0 к программе P.Тогда θ — правильный ответ на запрос G0 к программе P.
(Доказывается индукцией по длине вычисления)Теорема полноты. Пусть: 1)P = {D1, D2, …, DN} — хорновская логическая программа, 2) G0 =?C1, C2, …, Cm —запрос с множеством целевых переменных Y1, Y2, …, Yk, 3)θ — правильный ответ на запрос G0 к хорновскойлогической программе P.
Тогда существует такой вычисленный ответ η на запрос G0 к программе P, что θ = ηρдля некоторой подстановки ρ.Теорема сильной полноты: Каково бы ни было правило выбора подцелей R, если θ — правильный ответ назапрос G0 к хорновской логической программе P, то существует такой R-вычисленный ответ η, что равенство θ =ηρ выполняется для некоторой подстановки ρ.Деревом SLD-резолютивных вычислений запроса G0 к логической программе P называется помеченное корневоедерево TG0,P, удовлетворяющее следующим требованиям:1. Корнем дерева является исходный запрос G02.
Потомками каждой вершины G являются всевозможные SLD-резольвенты запроса G (прификсированном стандартном правиле выбора подцелей)3. Листовыми вершинами являются пустые запросы (завершающие успешные вычисления) и запросы, неимеющие SLD-резольвент (завершающие тупиковые вычисления).Определение правильного ответа: Пусть P — логическая программа, G — запрос к P с множеством целевыхпеременных Y1, …, Yk. Тогда всякая подстановка θ = {Y1/t1, …, Yk/tk} называется ответом на запрос G кпрограмме P. Ответ θ = {Y1/t1, …, Yk/tk} называется правильным ответом на запрос G к программе P, если P |=∀Z1.
. . ∀ZN Gθ, где {Z1, . . . , ZN} = ⋃=1 .Стратегией вычисления запросов к логическим программам называется алгоритм построения (обхода) дереваSLD-резолютивных вычислений TG0,P всякого запроса G0 к произвольной логической программе P.Стратегия вычислений называется вычислительно полной, если для любого запроса G0 и любой логическойпрограммы P эта стратегия строит (обнаруживает) все успешные вычисления запроса G0 к программе P.Стратегия обхода в ширину является вычислительно полной.Стратегия обхода в глубину является вычислительно не полной.Теорема Черча: не существует алгоритма, способного определить по заданной замкнутой формуле логикипредикатов ϕ, является ли эта формула общезначимой, т.
е. проблема общезначимости "| = ϕ ?"алгоритмическинеразрешима. (просто потому что иначе задача проверки является ли заданная подстановка – вычисленнымответом была бы алгоритмически разрешима, что привело бы к алгоритмической разрешимости задачиостанова МТ) (Следствие Теоремы Тьюринга об алгоритмической неразрешимости проблемы останова)Допущение Замкнутости Мира. Пусть имеется некоторое непротиворечивое множество замкнутых формул Γ(например, хорновская логическая программа) и замкнутая формула ϕ (например, запрос или отдельнаяподцель).
Тогда формула ¬ϕ является логическим следствием множества Γ в допущении замкнутости мира Γ|=CWA ¬ϕ, если неверно, что ϕ логически следует из Γ, т. е. Γ |≠ ϕ.(Здесь CWA — аббревиатура Closed World Assumption)Правило SLDNF-резолюцииПусть имеется запрос G0: ?not(C0), C1, …, Cn к программе P. Для вычисления SLDNF-резольвенты G11. формируется запрос G’: ? C0 к программе P;2. проводится построение (обход) дерева вычислений T запроса G’: ? C0;3. в зависимости от устройства дерева T возможен один из трех исходов:1. Успех. Дерево T конечно, и все его ветви (SLD-резолютивные вычисления) являются тупиковыми.2.
Неудача. При построении (обходе) дерева T было обнаружено успешное вычисление.3. Бесконечное вычисление. Дерево T бесконечно и при его построении (обходе) не былообнаружено успешных вычислений.Интуиционистская интерпретация — это реляционная система I = <S, R, ξ>, в которой1. S ≠ ∅ — множество состояний (состояний знания);2.
R ⊆ S × S — отношение переходов на S, которое является отношением нестрогого частичного порядка:1. рефлексивное R(s, s);2. транзитивное R(s1, s2)&R (s2, s3) ⇒ R(s1, s3);3. антисимметричное R(s1, s2) & R(s2, s1) ⇒ s1 = s2;3. ξ: S × P → {true, false} — оценка атомарных формул, удовлетворяющая условию монотонности:R (s1, s2) & ξ (P , s1) = true ⇒ ξ (P , s2) = true.Формула ϕ называется интуиционистски общезначимой (законом интуиционистской логики), если для любойинтерпретации I и для любого состояния s верно I, s |=I ϕ.Теорема (корректности SLDNF-резолюции): Если запрос G: ? not(C0) к хорновской логической программе P имеетуспешное SLDNF-резолютивное вычисление, то P |=CWA ¬∃y C0.Отношение выполнимости для модальных формул: Пусть I = <W , R, ξ> — модель Крипке.Тогда отношение выполнимости I, s |= ϕ формулы ϕ в мире s модели I определяется так:1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
