Теормин (2006) (1162014), страница 5
Текст из файла (страница 5)
SLD-резолютивное вычисление называется R-вычислением, если на каждомшаге вычисления очередная подцель выбирается по правилу R.18Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Определение. Вычисленный ответ, полученный в результате R-вычисления называется Rвычисленным ответом.Лемма (переключательная): Пусть Р – хорновская логическая программа, G0 - запрос кней, пусть также имеется SLD-резолютивное вычисление G0 , (G1 ,θ1 ),..., ( , θ n ) , причем G1 иG2 - этапы SLD-резолютивного вычисления, на которых i-ая подцель была раскрыта поправилу D1 и D2 соответственно.
Тогда существует SLD-резолютивное вычислениеG0 , (G '1 ,θ '1 ), (G '2 , θ '2 ),..., ( ,θ 'n ) , такое, что на этапе G '1 раскрытие происходило по правилуD2 , а на этапе G '2 - по правилу D1 , при этом для вычисленных ответов η и η ' существуютконечные подстановки ρ и ρ ' , такие, что η = η ' ρ ' , η ' = ηρ .Теорема: Пусть Р – хорновская логическая программа, G – запрос к ней, R и R' – различныеправила выбора. Тогда если η - R-вычислимый ответ на G к Р, то существует такой R'вычислимый ответ η ' , такой, что η = η ' ρ ' и η ' = ηρ для некоторых конечных перестановок(переименований) ρ и ρ ' .Теорема (сильной полноты): Пусть G – запрос к хорновской логической программе Р, R –правило выбора, θ - правильный ответ на G к Р.
Тогда существует R-вычислимый ответ η ,такой, что θ = ηρ , где ρ - конечная подстановка (переименование).Определение. Пусть G – запрос к хорновской логической программе Р, в которой всепрограммные утверждения упорядочены. Тогда деревом SLD-резолютивных вычисленийзапроса G к Р называется корневое упорядоченное (т.е. выходящие из любого узла дугипронумерованы) дерево, обладающее следующими свойствами:1) каждой вершине приписан запрос;2) корню дерева приписан запрос G;3) из каждой вершины, помеченной запросом G0 , исходят дуги, помеченныенатуральными числами 1 ≤ i1 ≤ ...
≤ ik ≤ N , где N – количество программныхутверждений в Р, и идущие в вершины, помеченные G1 , G2 ,..., Gk в том и только в томслучае, когда ∀l ∈ [1, k ] запрос Gl получен из запроса G путем примененияпрограммного утверждения Drl и при этом других SLD-резольвент, инцидентных G0 ,нет.Таким образом, каждая ветвь такого дерева будет соответствовать вычислению ответа назапрос G к логической программе Р.Определение. Стратегией вычисления называется стратегия обхода дерева SLDрезолютивных вычислений:• стратегия обхода в ширину: поярусное построение дерева. Как только в однойиз ветвей обнаруживается , то ответ вычисляется путем «сбора» всехподстановок на данной ветви;• стратегия обхода в глубину с возвратом – построение дерева по ветвям (накаждом этапе выбирается самая левая из непройденных ветвей)Определение.
Стратегия вычисления (обхода дерева SLD-резолютивных вычислений)называется полной, если для любого запроса G к логической программе Р все вычисленныеответы будут построены.19Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Теорема. Стратегия обхода в ширину – полная, стратегия обхода в глубину с возвратом –неполная.Определение.
Оператор отсечения (саt) – это 0-местный предикат со следующейоперационной семантикой:Пусть в логической программе РG0имеется программной утверждениеD : A0 ← A1 ,..., Ai ,!, Ai +1 ,..., An , G0 запрос к этой программе. Строим*дерево SLD-резолютивных вычислений.* - это парная метка, которая означает,G1 = ? A '0 , C1 ,..., Ck : ∃НОУ ( A '0 , A0 ) = θ что нас с момента ее появленияDинтересует только одна альтернатива.Соответственно, после второгоG2 = ?( A1 ,..., Ai ,!, Ai +1 ,..., An , C1 ,..., Ck )θпоявления * ветвление сноваразрешается.Откат при этом производится ввершину, предшествующую первому* G3 = ?!, A 'i +1 ,..., A 'n , C '1 ,..., C 'kпоявлению * .Теорема полноты для SLDрезолютивного вычисления с операциейG4 = ? A 'i +1 ,..., A 'n , C '1 ,..., C 'kотсечения не выполняется.Определение.
Оператор отрицания (not) – это оператор логического программирования соследующей операционной семантикой:Пусть Р – логическая программа, а G – запрос вида not(A). Тогда реакция интерпретатора наданный запрос будет следующей:1) если существует успешное SLD-резолютивное вычисление на запрос G ' : ? A , торезультатом вычисления будет fail;2) если SLD-резолютивное дерево вычислений для запроса G ' : ? A представляет собойконечное число неудачных ветвей, то запрос G имеет успешное вычисление;3) если интерпретатору не удалось обойти все ветви дерева за конечное число шагов (т.е.если в SLD-резолютивном дереве вычислений для запроса G ' : ? A присутствует хотябы одна бесконечная ветвь, а остальные неудачны), то ответом на запрос G будет ∞ .Таким образом, оператор not работает на основе «почти трехзначной» логики, что даетэффект немонотонности вывода.4.
Обзор разделов математической логики4.1. Исчисление предикатов и элементарная теорияИсчисление предикатов состоит из системы аксиом и правил вывода. Существует многоразных систем аксиом.Система аксиом:Ax1: ϕ → (ψ → ϕ )Ax 2 : (ϕ → (ψ → χ ) ) → ( (ϕ → ψ ) → (ϕ → χ ) ) - закон сложного силлогизма20Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Ax3 : ϕ &ψ → ϕAx 4 : ϕ &ψ → ψ- свойства конъюнкцииAx5 : ϕ → (ψ → (ϕ &ψ ) )Ax6 : ϕ → ϕ ∨ ψAx7 :ψ → ϕ ∨ ψ(Ax8 : (ϕ → χ ) → (ψ → χ ) → ( (ϕ ∨ ψ ) → χ )Ax9 : ϕ → ( ¬ϕ → ψ )Ax10 : (ϕ → ψ ) → ( (ϕ → ¬ψ ) → ¬ϕ ))- свойства дизъюнкции- законы противоречияAx11: ϕ ∨ ¬ϕ - закон исключенного третьего{ t } , где х свободна для t в ϕ .Ax13 : ϕ ( x) { x } → ∃xϕ ( x)tAx12 : ∀xϕ ( x) xAx14 : ∀x (ϕ → ψ ) → (ϕ → ∀xψ ); x ∉ VarϕAx15 : ∀x (ψ → ϕ ) → ( ∃xψ → ϕ )Правила вывода:ϕ ϕ →ψ1.- правило отделения (modus ponens); следствие импликации отделяется отψпосылки.2.ϕ- правило обобщения.∀xϕОпределение.
Логическим выводом в исчислении предикатов из множества формул Гназывается конечная последовательность формул ϕ1 , ϕ2 ,..., ϕn , такая, что для любого i ≥ 1- либо ϕi ⊆ Γ ;- либо ϕi - одна из 15 аксиом;- либо ϕi получается из предшествующих формул по правилу отделения или обобщения.Логический вывод – формализация понятия математического доказательства.Последняя формула ϕ n из последовательности логического вывода называется выводимой изГ и обозначается как Γ | − ϕ n .
Если Г – пустое множество, то ϕ n называется теоремойИПисчисления предикатов.Теорема (Гёделя; корректности и полноты для исчисления предикатов): Формулаявляется теоремой исчисления предикатов тогда и только тогда, когда она общезначима.Следствие из первой теоремы Гёделя: Математика – неаксиоматизируемая наука.21Математическая логика, сводка определений.
(с) 2006 GrGr (grgr@later.ru)4.2. Интуиционистская логикаИнтуиционистская логика (логика Брауэра) – это классическая логика, из аксиом которойисключен закон «исключенного третьего».Определение. Интуиционистская интерпретация – это тройка I int =< S , R, ξ > , гдеS – непустое множество альтернативных состояний (состояний знаний);R ⊆ S × S - отношение нестрогого частичного порядка, указывающее, что некотороесостояние знаний может быть достигнуто из другого и обладающее свойствамитранзитивности, антисимметричности и рефлексивности;ξ : S × P → {T , F } - оценка истинности (способность решать задачи в определенномсостоянии).Отношение выполнимости для интуиционистской логики будет выглядеть следующимобразом:I int , S |= p ⇔ ξ ( S , p ) = T⎧ I , S |= pI int , S |= p & q ⇔ ⎨ int⎩ I int , S |= q⎡ I , S |= pI int , S |= p ∨ q ⇔ ⎢ int⎣ I int , S |= qI int , S |= p → q ⇔ ∀S ' ∈ S : R( S , S ') & I int , S ' |= p ⇒ I int , S ' |= qI int , S |= ¬p ⇔ ∀S ' ∈ S : R ( S , S ') ⇒ I int , S ' |≠ pИзменяется и понятие логического закона.Определение.
Формула ϕ называется общезначимой с точки зрения интуиционистскойлогики (интуиционистски общезначимой, обозначается как | = ϕ ), если формула ϕ будетintвыполнима в любом состоянии S любой интерпретации I int =< S , R, ξ > .Утверждение. Если формула ϕ интуиционистски общезначима, то она общезначима и сточки зрения классической логики предикатов.Утверждение. Формулы p ∨ ¬p и ¬¬p → p интуиционистски невыполнимы.Замечание. Не существует ни одного содержательного математического утверждения, длякоторого нельзя было бы построить интуиционистского доказательства, однако вседоказательства должны показывать правильность утверждения явно (конструктивно),поэтому все доказательства получаются более сложными, а результатом любого такогодоказательства будет построение алгоритма.Утверждение (дизъюнктивное свойство интуиционистской логики). Интуиционистскаяобщезначимость формулы ϕ ∨ ψ эквивалентна интуиционистской общезначимости либо ϕ ,либо ψ .Утверждение.
Формула ∃xϕ ( x) общезначима тогда и только тогда, когда существует такойтерм t, что формула ϕ (t ) будет интуиционистски общезначимой.22Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)4.3. Логика ХоараПусть П – программа, RΠ - отношение между ее входными и выходными данными (т.е. еслипри поступлении на вход значения х программа выдает у, то выражение RΠ ( x, y ) являетсяистинным).Определение. Программа называется правильной, если на ее выходе всегда появляетсярезультат, находящийся в определенном отношении с входными данными (т.е.|= ∀xin (ϕ0 ( xin ) → ∃xout ( RΠ ( xin , xout ) & ϕ1 ( xin , xout ))) ).Определение.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
