Логическое следование. Теорема дедукции

 

 

Если для всех интерпретаций в которых одновременно истинны пропозициональные формулы F1,F2,…,Fn, пропозициональная формула G также истинна, то G является логическим следствием из пропозициональных формул F1,F2,…,Fn – это посылки, а G –логическое следование.

F1,F2,…,Fn ˫ G

Пример: (a+b)*(a-b)=a²-b²

Раскладываем

E1^{R1 распредел.закон} →E2^{R2 перемест.закон} →E3R3 ^{взаимоуничтожение} →E4^R4x*x=x2 →E5(G)

Теорема дедукции – основная теорема логического вывода.

Форумла G является логическим следствием формулы F1, F2,…, Fn тогда и только тогда, когда формула F1&F2&Fn→G является тавтологией.

 

Необходимость

 

Дано: ПФ G – логическое следствие, ПФ F1&F2&…&Fn.

Доказать: ПФ F1&F2&…Fn →G – тавтология.

Доказательство: Пусть I произвольная интерпретация.

1 случай.

F1, F2, …,Fn = истина на I. Следовательно F1&F2&…Fn = истина. G=истина т.к. является логическим следствием.

И→И

F1&F2&,…&Fn→G≡И следует из таблицы истинности импликации. Ч.т.д.

2 случай.

ПФ F1,F2,…,Fn = Л на I, следовательно F1&F2&…&Fn=Л

G=И, т.к. является логическим следствием

F1&F2&,..,&Fn→G≡ И следует из таблицы истинности. Ч.т.д.

 

Достаточность

 

Дано: ПФ F1&F2&…&Fn→ G = тавтология = И(истинная во всех интерпретациях)

Доказать: ПФ G – логическое следствие.

Доказательство:

Пусть I произвольная интерпритация.

Случай 1.

F1,F2,…Fn= И => F1&F2…&Fn=И

И→G ≡ И

F1&F2&…&Fn→G ≡ И, следовательно G=И следует из таблицы истинности импликации. Следовательно G-логическое следствие. Ч.т.д.

Случай 2.

F1,F2,…Fn= И => F1&F2…&Fn=Л

Л→G ≡ И

F1&F2&…&Fn→G ≡ И, следовательно G=И следует из таблицы истинности импликации. Следовательно G-логическое следствие. Ч.т.д.

 

Следствие из теоремы дедукции.

ПФ G является логическим следствием ПФ F1,F2,…,Fn тогда и только тогда, когда F1&F2…&Fn & ˉG является противоречием.

 

Поиск решений предикатных логических моделей. Дедуктивная схема принятия решений.

На языке логики предикатов знания о некоторой предметной области записанной в виде совокупности пропозициональной формулы(ПФ) образуют базу знаний в Prolog.

Запрос к этой базе знаний так же формулируются в виде ПФ, которые называются целевой ПФ или целевой функцией.

Принятие решений по данному вопросу сводятся к выяснению вопроса имеется ли логический вывод целевой ПФ из множества ПФ образующих базы знаний(Является ли целевая ПФ логического следствия из ПФ базы знаний). Такая задача называется задачей доказательства теорем.

ПФ G формальной теорией τ называется теоремой этой формальной теорией, если существует вывод теории τ, у которой последней формулой является G.

Такая задача называется задачей доказательства теорем, а систему решающей такую задачу называют дедуктивной системой (схемой) принятия решения.

Автоматизация логического вывода. Тезис Чёрча

 

Согласно теореме дедукции выяснение вопроса логического следствия целевой ПФ G из множества ПФ F₁,F₂…F_n сводится к доказательству общезначимости ПФ F₁&F₂&…&F_n->G или противоречивости ПФ согласно следствию F₁&F₂…&F_n & G.

В 1936 году американский физик Алонзо Чёрч доказал, что не существует единого алгоритма позволяющего установить общезначимость ПФ в исчислении предикатов первого порядка.

Результаты Чёрча оттеснили результаты работы Эрбрана, который предложил алгоритм позволяющий доказать общезначимость ПФ исчисления предикатов первого порядка, если она действительно является общезначимой, поэтому логику предикатов называют полуразрешимой системой.

В 1965 года Робинсон предложил основанный на методе Эрбрана метод резолюции.

 

Универсум Эрбрана и эрбрановская база

Современные процедуры связанные с автоматизации логического вывода, основывается на доказательстве следствия теоремы дедукции, т.е. F₁&F₂…&F_n & G является противоречием.

Составим множество S ПФ, которые включают в себя S={ F₁,F₂…F_n, G}.

Чтобы доказать противоречивость множества ПФ S нужно доказать, что не существует интерпретации, при которой все предложения истинны. Перебрать всевозможные интерпретации невозможно. Эрбран доказал, что существует подмножество Н, множество всех возможных интерпретаций, для которого множество ПФ S является противоречивым тогда и только, когда оно противоречиво для всех возможных интерпретаций. Подмножество Н - универсум Эрбрана и определяется следующим образом.

H₀ - множество констант, которые входят в множество S, если в множество S константы не входят, то в Н₀ включается любая константа. Тогда для i>0 Н_i есть множество H_i-1 объединённое со всеми элементами f_i(t_i,…t_j) образованными функциями f_i из множества S и элементами t_j, где j =1….n из H_i-1.

Множество H_i итым уровнем универсума Эрбрана.

Пример: S={P(x)\/ Q(a) ∨ P(f(x)), Q(b) ∨ P(g(x))}

H₀ ={a, b}

H₁ ={a, b, f (a), f(b), g(a), g(b)}

H₂ ={a, b, f (a), f(b), g(a), g(b), f(f(a)), f(f(b)), g(f(a)), g(f(b))}

 

Эрбрановская база множества предложений S – это множество всех константно-частных случаев атомных формул получающихся заменой всех их переменных элементами универсума Эрбрана.

В предыдущем примере в множестве S две атомных формулы Р(х) и Q(а).

{P(a), P(b), P(f(a)), P(f(b)), P(g(a)), P(g(b)), P(f(f(a))), P(f(f(b))), P(g(f(a))), P(g(f(b))), Q(a), Q(b), Q(f(a)), Q(f(b)), Q(g(a)), Q(g(b)), Q(f(f(a))), Q(f(f(b))), Q(g(f(a))), Q(g(f(b))). }

 

Классификация систем логического уровня

Классификация систем логического вывода.

Метод резолюции

Метод резолюции является более эффективным методом чем метод семантических деревьев.

Например: Y=sin(2x)

Z=2x

Y=sin(z)

Подстановка – замена переменных в некотором выражении на термы. Любую подстановку можно представить в виде множества упорядоченных пар N={t₁/V₁, t₂/V₂, ……., t_k/V_k}, где пара t_i/V_i означает что в выражении каждое вхождение переменной в V_i заменяется на терм t_i не содержащий эту переменную.

Пример:

N={r/2x}

Пример:

N1={z/x, w/y}

P(x, f(y), b}

P(x,f(y),b)_N1=P(z,f(w)

 

Унификация.

Применение подстановки N к множеству {E_ii} c целью приведения их к одному и тому же виду. Если такая подстановка N существует то такая подстановка называется унификатором для множества выражений Е итое, а само множество выражений называется унифицируемым.

E={P(x,f(y),b), P(x,f(b),t}

E₁=P(x,f(y),b)

E₂=P(x,f(y),b)

N={a/x,f(b/y),b)

E_1N=P(a,f(b),b)

E_2N=P(a,f(b),b)

M={b/y}

E_1N’={P(x,f(b),b)}

E_2N’={P(x,f(b),b)}