Теормин 2014 (микро) (Мадорский), страница 2

. . , tm из эрбрановского универсумаHσ. Тогда дизъюнкт D’ = (L1 ∨ · · · ∨ Lk){x1/t1, . . . , xm/tm}, полученный из D подстановкой основных термов t1, …,tmвместо всех переменных дизъюнкта D называется основным примером дизъюнкта D.Теорема Эрбрана: Система дизъюнктов S = {D1, . . . , DN} противоречива ⇐⇒ существует конечное противоречивоемножество G’ основных примеров дизъюнктов системы S.

(система противоречива <=> для каждой H-интерпретацииона противоречива, т.е. любой основной пример для некоторого дизьюнкта – ложен, а дальше - опираясь на теоремуКомпактности Мальцева, т.е. что всегда можно выделить конечное подмножество из множества)Пусть E1 и E2 — два логических выражения (термы, атомы, формулы и др.) Подстановка θ называется унификаторомвыражений E1 и E2, если E1θ = E2θ. Подстановка θ называется наиболее общим унификатором(НОУ) выражений E1 иE2, если: 1) θ — унификатор выражений E1 и E2, 2) для любого унификатора η выражений E1 и E2 существует такаяподстановка ρ, для которой верно равенство η = θρ.

НОУ(E1, E2) — множество наиболее общих унификатороввыражений E1 и E2. Подстановка θ называется унификатором системы уравнений E E: {t1 = s1; t2 = s2; …tn = sn} еслидля любого i , 1 ≤ i ≤ n, термы tiθ и siθ одинаковы. (Фактически, унификатор θ = {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.