Сводка определений - 2 (Старые варианты экзамена), страница 5

PDF-файл Сводка определений - 2 (Старые варианты экзамена), страница 5, который располагается в категории "к экзамену/зачёту" в предмете "математическая логика и логическое программирование" изседьмого семестра. Сводка определений - 2 (Старые варианты экзамена), страница 5 - СтудИзба 2019-09-18 СтудИзба

Описание файла

Файл "Сводка определений - 2" внутри архива находится в следующих папках: Старые варианты экзамена, 2010. PDF-файл из архива "Старые варианты экзамена", который расположен в категории "к экзамену/зачёту". Всё это находится в предмете "математическая логика и логическое программирование" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 5 страницы из PDF

Тогда существует 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 ))) ).Определение. Тройкой Хоара называется формула вида {ϕ } < Π > {ψ } , где ϕ ,ψ - формулы, аП – программа, причем если на входе программы П выполняется утверждение ϕ , то на еевыходе выполняется отношение ψ . Формула ϕ называется предусловием, формула ψ постусловием.Определение. Программа П называется частично корректной относительно предусловия ϕи постусловия ψ , если общезначима формула {ϕ } < Π > {ψ } . Эту общезначимость следуетпонимать следующим образом: для любой допустимой интерпретации I и любого наборазначений свободных переменных {α1 , α 2 ,..., α n } ∈ Varϕ ∪ Varψ из выполнимости формулы ϕ( I |= ϕ[d1 , d 2 ,..., d n ] ) будет следовать, что после завершения программы П переменныепримут значения d '1 , d '2 ,..., d 'n , причем формула ψ будет выполнима на данных значенияхпеременных ( I |= ψ [d1 , d 2 ,..., d n ] ).Определим модельный язык программирования:П ::=||||(x = t)П1, П2if A then П1 else П2 fiwhile A do П1 odeps,Где х – переменная, t – терм Пi – программы, А – атом, eps – пустота.F1 , F2 ,..., Fn, причемF0выражения в верхней части правила называются предпосылками, выражение в нижней частиправила называется заключением.

Свежие статьи
Популярно сейчас