Теормин 2014 (avasite), страница 5

(следует из предыдущих 2-х лемм)

Теорема Тьюринга об алгоритмической неразрешимости проблемы останова

Проблема останова машин Тьюринга алгоритмически неразрешима, т. е. не существует алгоритма (машины Тьюринга), способного вычислить следующую функцию

(доказательство знает каждый первокурсник)

Следствие 1.

Не существует алгоритма, способного определить по заданному запросу G к хорновской логической программе P,

1. является ли дерево SLD-резолютивных вычислений запроса G конечным;

2. содержит ли дерево SLD-резолютивных вычислений запроса G хотя бы одно успешное вычисление;

3. является ли заданная подстановка θ вычисленным ответом на запрос G .

Следствие 2 (Теорема Черча)

Не существует алгоритма, способного определить по заданной замкнутой формуле логики предикатов ϕ, является ли эта формула общезначимой, т. е. проблема общезначимости "| = ϕ ?"алгоритмически неразрешима.

(просто потому что иначе задача проверки является ли заданная подстановка – вычисленным ответом была бы алгоритмически разрешима, что привело бы к алгоритмической разрешимости задачи останова МТ)

Лекция 16. Управление вычислениями логических программ. Оператор отсечения.

Есть два основных способа управления вычислением логической программы:

1. Выбирать правильный порядок расположения атомов в телах процедур (по принципу: вначале решать простые задачи, а потом сложные).

2. Выбирать правильный порядок расположения программных утверждений (по принципу: вначале предлагать простые способы решения, а потом сложные).

Оператор отсечения

Для этого в языках логического программирования вводится оператор отсечения (cut). Этот оператор представляет собой 0-местный предикат !, оказывающий специальный побочный эффект.

С точки зрения декларативной семантики, предикат ! имеет постоянное значение true. Для его описания не требуется никаких программных утверждений (! — встроенный предикат). Поэтому оператор отсечения может использоваться в запросах и в телах программных утверждений, не оказывая при этом никакого влияния на их логический смысл.

Операционная семантика оператора отсечения ! задается следующими правилами:

1. Если запрос G и программное утверждение D: A₀ ← A₁, …, !, …, A_n порождают SLD-резольвенту G₀, то в стеке вычислений программы запрос G получает специальную служебную пометку (∗, индивидуальную для каждого вхождения оператора !

2. Если в запросе G оператор ! активен, т. е. G = ? !, C₁, …, C_k, то в стеке вычислений программы запрос G получает специальную служебную пометку ∗), индивидуальную для каждого вхождения оператора !, и при этом порождается новый запрос G₀ = ? C₁, …, C_k;

3. Если по ходу вычисления при откате достигается элемент стека вычислений программы, помеченный ∗), то из стека удаляются все элементы, расположенные между элементами, помеченными (∗ и ∗) (включая и сами эти элементы).

Программное утверждение A₀ ← A₁, …, A_k, !, A_k+1, …, A_n содержащее оператор отсечения можно прочитывать двояко:

1. Чтобы решить задачу A₀ нужно найти только первое решение задач A₁, …, A_k и далее решать задачи A_k+1, …, A_n. Если решение задач A₁, …, A_k найти не удается, то воспользоваться альтернативными процедурами решения задачи A₀.

2. Чтобы решить задачу A₀ нужно проверить условия A₁, …, A_k. Если эти условия выполнены, то приступить к решению задач A_k+1, .., A_n и не обращаться к другим вариантам решения задачи A₀. Если же эти условия не выполнены, то обратиться к альтернативным способам решения задачи A₀.

Таким образом, оператор отсечения позволяет удобно использовать в логическом программировании стандартные конструкции императивного программирования.

1. Ветвление. S₀: if P then S₁ else S₂ fi

P_{if−then−else}: S₀ ← P, !, S₁; S₀ ← S₂;

1. Итерация. S₀: while P do S₁ od

P_while−do: S₀ ← P, !, S₁, S₀; S₀ ←;

Лекция 17. Отрицание в логическом программировании. Оператор not. Встроенные предикаты и фукнции. Оператор вычисления значений. Модификация баз данных.

Допущение Замкнутости Мира. Пусть имеется некоторое непротиворечивое множество замкнутых формул Γ (например, хорновская логическая программа) и замкнутая формула ϕ (например, запрос или отдельная подцель). Тогда формула ¬ϕ является логическим следствием множества Γ в допущении замкнутости мира Γ |=_CWA ¬ϕ, если неверно, что ϕ логически следует из Γ, т. е. Γ |≠ ϕ.

(Здесь CWA — аббревиатура Closed World Assumption)

Правило SLDNF-резолюции

Пусть имеется запрос G₀: ?not(C₀), C₁, …, C_n к программе P. Для вычисления SLDNF-резольвенты G₁

1. формируется запрос G’: ? C₀ к программе P;

2. проводится построение (обход) дерева вычислений T запроса G’: ? C₀;

3. в зависимости от устройства дерева T возможен один из трех исходов:

   1. Успех. Дерево T конечно, и все его ветви (SLD-резолютивные вычисления) являются тупиковыми.

   2. Неудача. При построении (обходе) дерева T было обнаружено успешное вычисление.

   3. Бесконечное вычисление. Дерево T бесконечно и при его построении (обходе) не было обнаружено успешных вычислений.

Теорема (корректности SLDNF-резолюции)

Если запрос G: ? not(C₀) к хорновской логической программе P имеет успешное SLDNF-резолютивное вычисление, то P |=_CWA ¬∃y C₀.

(Есть успешное вычисление т.е. древе разбора – все тупики, т.е. не существует такой подстановки, что бы в какой-нибудь интерпретации выводилось бы С₀ т.е. из P не следует С₀ т.е. по определению CWA следует то, что нужно)

Лекция 18. Итуиционистская логика.

Интуиционизм — это философское течение в математике, возникшее в начале 20 века как критический отклик на неограниченное применение формальных логических методов в математике, приводящее к парадоксам (антиномиям). По мнению интуиционистов (Брауэр, Вейль, Пуанкаре), парадоксы возникают в связи с тем, что законы логики, справедливые для конечных множеств, безосновательно переносятся на бесконечные множества.

Семантика Колмогорова–Брауэра–Гейтинга

1. ϕ & ψ: Решить обе задачи ϕ и ψ и предъявить решение;

2. ϕ ∨ ψ: Выбрать одну из двух задач ϕ и ψ, решить выбранную задачу и предъявить решение;

3. ϕ → ψ: Показать, что решение задачи ψ сводится к решению задачи ϕ, т. е. предъявить способ, который позволяет, располагая решением задачи ϕ, построить решение задачи ψ;

4. ¬ ϕ: Доказать, что задача ϕ не имеет решения. Законами интуиционистской логики считаются только те формулы, которые соответствуют описаниям составных задач, имеющих решение при любых условиях.

Законы интуиционистской логики

1. P → P — каждую задачу можно свести к ней самой;

2. (P → Q) & (Q → R) → (P → R) — чтобы свести задачу R к задаче P достаточно найти задачу Q, к которой можно свести задачу R, и которую, в свою очередь, можно свести к задаче P;

3. P → ¬¬P — чтобы убедиться в том, что не существует доказательства неразрешимости задачи P, достаточно найти решение задачи P;

4. (¬P ∨ ¬Q) → ¬(P &Q) — чтобы показать, что обе задачи P и Q нельзя решить одновременно, достаточно выбрать одну из этих задач и показать, что она неразрешима.

Определение (модель Крипке)

Пусть P = {P1, P2, …, Pn, …} — множество атомарных формул (названия задач).

Интуиционистская интерпретация — это реляционная система 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, R, ξ> — интуиционистская интерпретация. Тогда отношение выполнимости I, s |=_I ϕ формулы ϕ в состоянии s интерпретации I определяется так:

1. если ϕ = P ∈ P, то I, s |=_I ϕ ⇐⇒ ξ (s, P) = true;

2. I, s |=_I ϕ₁&ϕ₂ ⇐⇒ I, s |=_I ϕ₁ и I, s |=_I ϕ₂;

3. I, s |=_I ϕ₁ ∨ ϕ₂ ⇐⇒ I, s |=_I ϕ₁ или I, s |=_I ϕ₂;

4. I, s |=_I ϕ₁ → ϕ₂ ⇐⇒ для любого состояния s’, если (s, s’) ∈ R и I, s’|=_I ϕ₁, то I, s’|=_I ϕ₂;

5. I, s |=_I ¬ϕ₁ ⇐⇒ для любого состояния s', если(s, s') ∈ R, то I, s' |≠_I ϕ₁.

Формула ϕ называется интуиционистски общезначимой (законом интуиционистской логики), если для любой интерпретации I и для любого состояния s верно I, s |=_I ϕ.

Теорема 1

|=_I ϕ ⇒ |=_C ϕ

Теорема 2 (дизъюнктивное свойство)

|=_I ϕ ∨ ψ ⇐⇒ |=_I ϕ или |=_I ψ

Теорема 3 (экзистенциальное свойство)

|=_I ∀x1 …∀x1∃y ϕ(x₁, …, x_n, y) ⇐⇒ существует такой терм t(x₁, …, x_n), что |=_I ϕ(x₁, …, x_n, t(x₁, …, x_n))

t(x₁, ..., x_n) — это программа решения задачи ϕ.

Это называется «изоморфизмом Карри–Ховарда».

Лекция 19. Модальные логики.

Синтаксис модальных формул

Расширим синтаксис классической логики предикатов, введя два логических оператора:

1. □ (модальность необходимого) и

2. ◊ (модальность возможного),

при помощи которых разрешается строить формулы следующего вида:

1. (□ϕ) «необходимо ϕ»,

2. (◊ϕ) «возможно ϕ».

Семантика Крипке модальных формул

Определим самое общее отношение выполнимости для модальных формул.

Пусть P = {P1, P2, …, Pn, …} — множество атомарных формул (элементарные высказывания).

Модальная интерпретация или модель Крипке — это реляционная система I = <W, R, ξ>, в которой

1. W ≠ ∅ — множество состояний (возможные миры);

2. R ⊆ W × W — отношение достижимости на W,

3. ξ: W × P → {true, false} — оценка атомарных формул.

Система <W, R> называется шкалой Крипке (frame).

Если (w, w') ∈ R, то возможный мир w' называется альтернативным миром для w.

Отношение выполнимости для модальных формул

Пусть I = <W , R, ξ> — модель Крипке.

Тогда отношение выполнимости I, s |= ϕ формулы ϕ в мире s модели I определяется так:

1. если ϕ = P ∈ P , то I, s |= ϕ ⇐⇒ ξ (w, P) = true;

2. I, w |= ϕ₁&ϕ₂ ⇐⇒ I, w |= ϕ1 и I, w |= ϕ2;

3. I, w |= ϕ₁ ∨ ϕ₂ ⇐⇒ I, w |= ϕ₁ или I, w |= ϕ₂;

4. I, w |= ϕ₁ → ϕ₂ ⇐⇒ I, w |≠ ϕ₁ или I, w |= ϕ₂;

5. I, w |= ¬ϕ₁ ⇐⇒ I, w |= ϕ₁;

6. I, w |= □ϕ ⇐⇒ для любого альтернативного мира w' если <w, w’> ∈ R, то I, w'|= ϕ;

7. I, w |= ◊ϕ ⇐⇒ существует такой альтернативный мир w', что <w, w'> ∈ R и I, w' |= ϕ.

Свойства:

1. |= ◊ϕ ≡ ¬□¬ϕ;

2. |= □ (ϕ1 → ϕ2) → (ϕ1 → ϕ2);

3. |= ϕ ⇒ |= □ϕ (правило необходимости).

Характеристические формулы

1. □ϕ → ϕ рефлексивные шкалы ∀w R(w, w);

2. □ϕ → □□ϕ транзитивные шкалы ∀w₁∀w₂∀w₃ (R(w₁, w₂)&R(w₂, w₃) → R(w₁, w₃));

3. ◊□ϕ → □ϕ симметричные шкалы ∀w₁∀w₂ (R(w₁, w₂) → R(w₂, w₁)).

Эпистемические логики и мультагентные системы

Эпистемические логики — это разновидности модальных логик, изучающие модальности знания и мнения (веры) идеализированных агентов. Интерес представляют вопросы о том, какими знаниям располагает субъект, насколько он осознает свои знания (и незнания), и какие причинно-следственные связи возникают между утверждениями, касающимися вопросов знания и веры. В эпистемической логике модальный оператор □ϕ следует прочитывать «Я знаю, что ϕ», а ◊ϕ — «Я допускаю, что ϕ».

Эпистемические логики и мультагентные системы

Основные законы (аксимы) эпистемической логики:

1. Аксиома адекватности знания: □ϕ → ϕ

«Мои знания верны».

1. Аксиома позитивной интроспекции: □ϕ → □□ϕ

«Я вполне представляю все, что мне известно».

1. Аксиома негативной интроспекции: ◊□ϕ → □ϕ

«Я вполне сознаю, что именно мне неизвестно».

Пусть A = {a₁, a₂, …, a_n} — множество агентов. Тогда

□_a ϕ означает «Агент a знает, что ϕ верно».

□_C ϕ означает «Все агенты знают, что ϕ верно».