Теормин (2006) (1162014), страница 2
Текст из файла (страница 2)
Правилом табличного вывода называется фигура видаT0.T1 (T2 )Введем следующую систему правил:< ¬ϕ , Γ | Δ >1. L¬ :. L означает, что мы преобразовываем левую часть таблицы, причем< Γ | ϕ, Δ >отрицание – главная логическая связка в формуле ϕ.6Математическая логика, сводка определений.
(с) 2006 GrGr (grgr@later.ru)< Γ | ¬ϕ , Δ >.< ϕ, Γ | Δ >< ϕ1 & ϕ 2 , Γ | Δ >3. L & :.< ϕ1 , ϕ 2 , Γ | Δ >< Γ | ϕ1 & ϕ 2 , Δ >4. R & :. В данном случае происходит ветвление процесса табличного< Γ | ϕ1 , Δ >< Γ | ϕ 2 , Δ >вывода, и выполнимость Т0 эквивалентна выполнимости или Т1, или Т2.< ϕ1 ∨ ϕ 2 , Γ | Δ >5. L ∨ :.< ϕ1 , Γ | Δ >< ϕ 2 , Γ | Δ >< Γ | ϕ1 ∨ ϕ 2 , Δ >6. R ∨ :.< Γ | ϕ1 , ϕ 2 , Δ >< ϕ1 → ϕ 2 , Γ | Δ >7. L → :.< ϕ 2 , Γ | ϕ1 , Δ >< Γ | ϕ1 → ϕ 2 , Δ >8.
R → :.< ϕ1 , Γ | ϕ 2 , Δ >2. R¬ :С помощью данных правил можно существенно упростить таблицу. Для упрощения формулс кванторами требуется ввести дополнительные понятия.Определение. Подстановкой называется любое отображение θ : Var → Term . Областьюподстановки называется множество Domθ = {x : θ ( x) ≠ x} . Если область подстановкиконечна, то такая подстановка называется конечной. Множество всех конечных подстановокбудем обозначать как Subst.
Если θ - конечная подстановка, то она представима в видеxnxx2множества связок: θ = { 1θ ( x1 ) , θ ( x2 ) ,..., θ ( xn )} .Определение. Пусть Е – логическое выражение θ - постановка θ = { x } . Тогда запись видаtЕθ будет называться результатом применения подстановки θ к Е. Он определяетсяследующим образом:⎧ t, y ≡ x1) Е – переменная ( E = y ∈ Var ). Тогда Eθ = ⎨= θ ( y) .⎩ y, y ≠ x2) Е – константа (Е = с). Тогда Eθ = E .3) Е – составной терм ( E = f (t1 , t2 ,..., tk ) ). Тогда Eθ = f (t1θ , t2θ ,..., tkθ ) .4) Е – атомарная формула ( E = P(t1 , t2 ,..., tk ) ).
Тогда Eθ = P (t1θ , t2θ ,..., tkθ ) .5) Е – формула вида ϕ1 • ϕ 2 , где • означает конъюнкцию, дизъюнкцию или импликацию.Тогда Еθ = ϕ1θ • ϕ2θ , а если Е – формула вида ¬ ϕ , то Eθ = ¬ϕθ .⎧ E, y ≡ x⎪6) Е – формула с квантором ∀yϕ или ∃yϕ . Тогда Eθ = ⎨∀.yϕθ,y≠x⎪∃⎩Определение. Переменная х является свободной для терма t в формуле ϕ, если в ϕ нетсвободных вхождений переменной х в области действия кванторов, связывающихпеременные из множества Vart (множества переменных терма t).На основе понятия подстановки введем 4 новых правила табличного вывода:7Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)< ∀xϕ ( x), Γ | Δ >при условии, что переменная х в формуле ϕ(х) свободна< ∀xϕ ( x), ϕ ( x){ x }, Γ | Δ >tдля терма t.< Γ | ∀xϕ ( x), Δ >10.
R∀ :, где с – это константа, которая не содержится в Г, Δ или ϕ(х).< Γ | ϕ ( x){ x }, Δ >c< ∃xϕ ( x), Γ | Δ >11. L∃ :.< ϕ ( x){ x }, Γ | Δ >c< Γ | ∃xϕ ( x), Δ >12. R∃ :< Γ | ∃xϕ ( x), ϕ ( x){ x }, Δ >tТаким образом, имеем 12 правил, располагая которыми, можно построить табличный вывод.9. L∀ :Определение. Табличным выводом семантической таблицы Т0 называется корневое дерево,вершины которого помечены таблицами, причем это дерево удовлетворяет следующимтребованиям:1. Корневая вершина помечена таблицей Т0.2.
Каждая висячая вершина должна быть помечена либо закрытой таблицей, либо такойтаблицей, что в ней содержатся только атомарные формулы (т.е. без связок и кванторов).3. Не висячая вершина, помеченная таблицей Тi, обязательно имеет одного или двухнаследников, которые получаются из Тi по одному из 12 правил табличного вывода.Дерево (или вывод) считается успешным (успешный вывод называется доказательством),если каждая ветвь дерева завершается закрытой таблицей.Для табличного вывода как для доказательства общезначимости сразу возникают следующиевопросы:- корректности;- полноты (является ли табличный вывод универсальным способом доказательства);- эффективности (каким образом и в каком порядке следует применять правила табличноговывода).Теорема (корректности): Если таблица Т0 имеет успешный табличный вывод, то Т0невыполнима.Следствие 1. Если таблица Tϕ =< ∅,{ϕ} > имеет успешный табличный вывод, то формула ϕобщезначима.Следствие 2.
Если таблица Tϕ' =< {ϕ}, ∅ > имеет успешный табличный вывод, то формула ϕявляется противоречивой.Теорема (полноты табличного вывода): Если таблица Т0 невыполнима, то Т0 имеетуспешный табличный вывод.Следствие 1 (теорема Гёделя о полноте): Если формула ϕ общезначима, то таблицаTϕ =< ∅,{ϕ} > имеет успешный табличный вывод.Следствие 2 (теорема Ливенгейма-Сколема о счетной модели): Если формула ϕвыполнима, то ϕ имеет модель с не более, чем счетной бесконечной областьюинтерпретации.Следствие 3 (теорема Мальцева о компактности): Пусть Γ ⊆ Form - произвольноемножество формул.
Тогда Г имеет модель тогда и только тогда, когда каждое ееподмножество имеет модель.Доказательство утверждения предлагается провести самостоятельно.8Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)2. Метод резолюцийМетод резолюций – один из наиболее эффективных способов автоматическогодоказательства теорем. Общие принципы доказательства утверждений с помощью методарезолюций таковы:1. Если мы хотим доказать общезначимость формулы ϕ, то для этого достаточно показать,что формула ϕ1 = ¬ϕ противоречива (т.е. провести доказательство от противного).2.
Формула ϕ1 приводится к предваренной нормальной форме ϕ2, в которой все кванторыстоят в начале формулы.3. Формула ϕ2 приводится к сколемовской стандартной форме, в которой отсутствуюткванторы существования: ϕ3 = ∀x1∀x2 ...∀xn ( D1 & D2 &...& Dn ) , где Di = L1 ∨ L2 ∨ ... ∨ Lm , а⎧ A⎫L j = ⎨ ⎬ . Следует убедиться, что содержимое ϕ не было потеряно.⎩ ¬A ⎭4. Доказательство общезначимости ϕ сводится к доказательству противоречивости системыдизъюнктов S = {D1 , D2 ,..., Dn } . Для этого применяется правило резолюций Робенсона:{D '∨ L, D ''∨ ¬L} ⇒ {D '∨ D '' = ∅} . Чтобы применение этого правила стало возможным,Робенсон ввел алгоритм унификации для системы {D '∨ L ', D ''∨ ¬L ''} .
Если L’ и L’’унифицированы, то такой метод построения вывода для общезначимой формулы станетполным.Введем новую связку ϕ ≡ ψ , которая эквивалентна формуле (ϕ → ψ ) & (ψ → ϕ ) .Определение. Формулы ϕ и ψ называются равносильными, если общезначима формулаϕ ≡ψ .Утверждение. Отношение равносильности является отношением эквивалентности.Утверждение. Если формулы ϕ и ψ равносильны, то:1. Из общезначимости ϕ следует общезначимость ψ;2.
Из выполнимости ϕ следует выполнимость ψ;3. Если I является моделью для ϕ, то она является также моделью для ψ.Теорема: Следующие пары формул являются равносильными:1) |= (ϕ → ψ ) ≡ (¬ϕ ∨ ψ )&&2) |= (ϕ ψ ) ≡ (ψ ϕ )∨∨& && &3) |= (ϕ (ψ χ )) ≡ ((ϕ ψ ) χ )∨ ∨∨ ∨&4) |= (ϕ ϕ ) ≡ ϕ∨∨ &∨ & ∨5) |= (ϕ (ψ χ )) ≡ (ϕ ψ ) (ϕ χ )& ∨& ∨ &6) |= ¬¬ϕ ≡ ϕ&∨7) |= ¬(ϕ ψ ) ≡ (¬ϕ ¬ψ )∨&9Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru){ y}); у не содержится в ϕ ( х)8) |= ∀xϕ ( x) ≡ ∀y (ϕ ( x) x∀∃9) |= ¬( xϕ ) ≡ x(¬ϕ )∃∀∀&∀&10) |= ( xϕ ) ψ ≡ x(ϕ ψ )x ∉ Varψ∃∨∃∨&&11) |= ∀x(ϕ ψ ) ≡ (∀xϕ ) (∀xψ )∨∨Определение. Запись ϕ [ψ ] означает, что в формуле ϕ содержится подформула ψ; записьϕ ⎡ψ χ ⎤ означает замену в формуле ϕ подформулы ψ на χ.⎢⎣⎥⎦Теорема: Пусть ϕ, ψ, χ - произвольные формулы. Тогда из равносильности ψ и χ следует,что |= ϕ ≡ ϕ ⎡ψ ⎤ .⎢⎣ χ ⎥⎦Определение.
Литера – это либо атом A = P(t1 , t2 ,..., tn ) , либо ¬A .Определение. Дизъюнкт – это либо дизъюнкция атомов L1 ∨ L2 ∨ ... ∨ Ln , либо пустойдизъюнкт - тождественная ложь.Определение. Предваренная нормальная форма – это формула видаQ1 x1Q2 x2 ...Qn xn M ( x1 , x2 ,..., xn ) , где Qi ∈ {∀, ∃} - кванторная приставка, а М – бескванторнаяформула (матрица), являющаяся КНФ вида D1 & D2 &...Dn , где Di – непустой дизъюнкт.Теорема (о предваренной нормальной форме): Для любой замкнутой формулы ϕсуществует равносильная ей предваренная нормальная форма ψ.Определение. Сколемовская стандартная форма – это предваренная нормальная формавида ∀x1∀x2 ...∀xn M ( x1 , x2 ,..., xn ) .Теорема (о сколемовской стандартной форме): Для любой замкнутой формулы ϕсуществует сколемовская нормальная форма ψ, причем ϕ выполнима тогда и только тогда,когда выполнима ψ.Лемма (о сколемизации): Пусть замкнутая формула ϕ имеет вид∀x1∀x2 ...∀xk ∃y χ ( x1 , x2 ,..., xk , y ) и пусть также имеется функциональный символ f ( k ) .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
