Ещё одни лекции В.А. Захарова, страница 38

Выделить множество V всех вершин графа Γϕ1 ,M , изкоторых достижимы радужные компоненты сильнойсвязности.6. Выделить множество V всех вершин (s0 , B0 ), для которойвыполняется s0 ∈ S0 , ϕ1 ∈/ B0 .7. Вычислить V = V ∩ V .Результат: M |= ϕ ⇐⇒ V = ∅.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПример.ϕ = pUqLTS M:'s1'- iξ(s1 ) = {p} 6&s0$s2?i$ξ(s2 ) = {q}%yξ(s0 ) = {p}'s3&- iξ(s3 ) = {p} 6&$s4?iξ(s4 ) = {p}%%АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПример.ϕ = F(pUq)1. Позитивная форма ϕ1 = pUqFLSubϕ1 = {p, ¬p, q, ¬q, pUq, X(pUq)};XSubϕ1 = {X(pUq)};URSubϕ1 = {pUq}.АЛГОРИТМ ВЕРИФИКАЦИИ2.

Строим систему Хинтикки Γϕ1 ,Mi{¬p, q}6' %s1s2?i'- i{p, ¬q,6{¬p, q}- ?is1{p, ¬q}'s2ϕ1 , Xϕ1 }s0{p, ¬q}is0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 6s4?is3{p, ¬q}- is36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}i%АЛГОРИТМ ВЕРИФИКАЦИИ3. Раскрашиваем вершины системыΓ ϕ1 ,M- ?ys1{p, ¬q}y{¬p, q}6' %s1s2?y'- i{p, ¬q,6{¬p, q}'s2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 6s4?is3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ4. Выделяем радужные компонентысильнойсвязности- ?ys1{p, ¬q}{¬p, q}y6' %s1s2?y'- i{p, ¬q,6{¬p, q}'s2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 64?sis3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ5. Выделяем вершины из которыхдостижимырадужные компоненты- ?is1{p, ¬q}{¬p, q}y6' %s1s2?y'- y{p, ¬q,6{¬p, q}'s2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }y&- i{p, ¬q} 64?sis3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ6.

Ищем вершину (s0 , B) на которойопровергаетсяϕ1'- ?is1{p, ¬q}{¬p, q}y6' %s1s2?y'- y{p, ¬q,6{¬p, q}s2ϕ1 , Xϕ1 }$$ϕ1 , Xϕ1 }s0s0yy{p, ¬q}{p, ¬q,ϕ1 , Xϕ1 }&- i{p, ¬q} 64?sis3ϕ1 , Xϕ1 }&{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММОписанный здесь подход к верификации распределенныхпрограмм реализован в программно-инструментальной системеверификации SPIN .Модели параллельных взаимодействующих процессовописываются на языке PROMELA (Process Meta Language),снабжаются темпоральными спецификациями (PLTLформулами), а затем выполнимость этих формул проверяетсясистемой верификации SPIN .В системе SPIN применяется табличный алгоритмверификации моделей распределенных программ.

Дляповышения его эффективности используется ряд приемов: проверка модели «на лету»; редукции частичных порядков; символьное представление данных и др.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММБолее подробно о системе верификации SPIN вам расскажутКонстантин Олегович СавенковиИгорь Владимирович Конновв курсе«Верификация программ на моделях»в весеннем семестре.КОНЕЦ ЛЕКЦИИ 22ЭКЗАМЕН СОСТОИТСЯ 11ЯНВАРЯ в 10 часов.КОНСУЛЬТАЦИЯ — 10 ЯНВАРЯв 15 часов.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

ЗахаровЛекция 18.Как устроена математика.Исчисление предикатов первогопорядка.Аксиоматические теории.Элементарная геометрия.Теория множествЦермело–Френкеля.Арифметика Пеано.Теорема Геделя о неполноте.модальныелогикиy6интуиционистскаялогикаyI@@@другая@другиелогическиеоперациисемантика@логических@связокyдругие кванторылогикивысших порядков@@@iтеориядоказательствyдругиеформылогическоговыводаспециальные интерпретации-КЛАССИЧЕСКАЯЛОГИКАyаксиоматическиетеорииКак устроена математикаМатематика — это специфическая наука.Она не относится к числу естественных наук (физика,ботаника, геология, и пр.), т.

к. она не имеет дела ни сприродными явлениями, ни с эмпирическими знаниями.Она не относится к числу гуманитарных наук (философия,история, политология и пр. болтология), т. к она не занимаетсяни людской деятельностью, ни людскими воззрениями.Она занимается созданием, развитием и изучениемматематических теорий — умозрительных конструкций,которые строятся по строгим объективным законамформальной логики .Как устроена математикаСтанислав Лем сравнивал математику сбезумным портным, который шьет одеждудля неведомых существ.Портного не беспокоит, кому придетсявпору его одежда.Он лишь хочет, чтобы платье было сшитопрочно.Как устроена математикаС чего начинается рассказ о каждом разделе математики?Вначале уславливаются о системе обозначений,определяют язык, на котором будут записыватьматематические утверждения (определяется синтаксисматематического языка ).Затем приходят к соглашению об основополагающихсвойствах, законах, которым должны удовлетворятьинтересующие нас операции и отношения надвоображаемыми объектами (формулируются аксиомыматематической теории ).Далее договариваются о том, какие средства обоснованияистинности математических утверждений считаютсядопустимыми (определяется аппарат логического вывода ).И после этого приступают к получению логическиобоснованных утверждений сформулированнойматематической теории (вывод теорем ).Вот так строятся формальные аксиоматические теории .Классическое исчисление предикатовКак можно аксиоматизировать теорию общезначимыхутверждений (формул)? Например, так:АКСИОМЫ.1.

Ax1. ϕ1 → (ϕ2 → ϕ1 ),2. Ax2. (ϕ1 → (ϕ2 → ϕ3 )) → ((ϕ1 → ϕ2 ) → (ϕ1 → ϕ3 )),3. Ax3. (ϕ1 & ϕ2 ) → ϕ1 ,4. Ax4. (ϕ1 & ϕ2 ) → ϕ2 ,5. Ax5. ϕ1 → (ϕ2 → (ϕ1 & ϕ2 )),6. Ax6. ϕ1 → (ϕ1 ∨ ϕ2 ),7. Ax7. ϕ2 → (ϕ1 ∨ ϕ2 ),8. Ax8. (ϕ1 → ϕ0 ) → ((ϕ2 → ϕ0 ) → ((ϕ1 ∨ ϕ2 ) → ϕ0 )),9. Ax9. ϕ1 → (¬ϕ1 → ϕ0 ),10. Ax10. ϕ1 ∨ ¬ϕ1 ,Классическое исчисление предикатовАКСИОМЫ.1. Ax11. ∀X ϕ(X ) → ϕ(t),2. Ax12. ϕ(t) → ∃X ϕ(X ),3. Ax13. ∀X (ϕ1 → ϕ2 (X )) → (ϕ1 → ∀X ϕ2 (X )),4. Ax14. ∀X (ϕ1 (X ) → ϕ2 ) → (∃X ϕ1 (X ) → ϕ2 ).ПРАВИЛА ВЫВОДА.1. Правило отделения (modus ponens)ϕ2. Правило обобщения∀X ϕϕ, ϕ → ψ,ψКлассическое исчисление предикатовЛОГИЧЕСКИЙ ВЫВОД.Пусть задано некоторое множество формул (гипотез) Γ .Тогда логическим выводом из множества гипотез Γназывается конечная последовательность формулϕ1 , ϕ2 , .

. . , ϕn ,в которой каждая формула ϕi удовлетворяет одному изследующих условий:1. либо ϕi является аксиомой,2. либо ϕi является гипотезой, т. е. ϕi ∈ Γ ,3. либо ϕi получается из предшествующих формул этойпоследовательности по правилу отделения или по правилуобобщения.В этом случае формула ϕn называется выводимой измножества Γ , и этот факт обозначается Γ ! ϕnФормула ϕ называется теоремой , если ∅ ! ϕ , и этот фактКлассическое исчисление предикатовИсчисление предикатов с равенством.Введем специальный двухместный предикатный символ = идобавим к аксиомам КИП следующие аксиомы равенства:1.

Ax15. ∀X (X = X ),2. Ax16 ∀X , Y (X = Y → (ϕ(X , X ) → ϕ(X , Y ))).Полученную систему аксиом называют классическимисчислением предикатов с равенством КИП= .Алгебраическая система I называется нормальнойинтерпретацией , если для любой пары различных предметовd1 , d2 из области интерпретации DI верно соотношениеI |= d1 = d2 .Аксиоматические теории первого порядкаЭлементарная аксиоматическая теория образуется изисчисления предикатов с равенством за счетограничения сигнатуры языка логики предикатовфиксированным конечным набором констант,функциональных и предикатных символов, обозначающихбазовые объекты, операции и отношения теории,добавления к множеству аксиом исчисления предикатовспециальных (нелогических) аксиом, описывающихбазовые принципы теории.Таким образом образуются элементарная теория равенства,элементарная теория групп, элементарная теория полей,элементарная геометрия, элементарная арифметика,элементарная теория множеств, и др.Формулы ϕ , логически выводимые из аксиом элементарнойаксиоматической теории T , называются теоремами этойтеории и обозначаются записью T ! ϕ .Аксиоматические теории первого порядкаЭлементарная аксиоматическая теория T называетсянепротиворечивой , если не все формулы являютсятеоремами теории T , т.

е. существует такая формула ϕ ,для которой T ! ϕ ;полной , если всякая формула или ее отрицание являютсятеоремами теории T , т. е. для любой формулы ϕ либоT ! ϕ , либо T ! ¬ϕ ;категоричной , если любые нормальные две моделитеории T изоморфны, т. е. для любой пары нормальныхинтерпретаций I1 , I2 верноI1 |= T и I2 |= T =⇒ I1 ∼= I2 ;разрешимой , если существует алгоритм, проверяющий,является ли произвольная формула теоремой теории T .Аксиоматическое устройство геометрииВпервые попытку аксиоматизировать геометрию предпринялЕвклид (3 в.

до н. э.). Геометрическая теория Евклидаопиралась на 5 аксиом.К сожалению, система геометрических аксиом из «Начал»Евклида неполна.Вот пример истинного утверждения, которое нельзя вывести изаксиом и постулатов Евклида.Если прямая пересекает одну из сторон треугольника в точке,отличной от вершины треугольника, то эта прямая такжепересекает еще одну сторону треугольника.tt@@@@@@tАксиоматическое устройство геометрииСистематическое и основательное построение геометрическойсистемы аксиом было осуществлено Д. Гильбертом (40 аксиом)в 1899 г.

Более более краткую аксиоматику удалось построитьА. Тарскому и его ученика (12 аксиом).Аксиомы ТарскогоБудем рассматривать геометрический мир, все объектыкоторого — точки .На множестве точек есть всего лишь два базовых предиката:B(x, y, z)точка y лежит между точками x и z наодной прямойD(x, y, z, u)точка x отстоит от точки y на такое жерасстояние, что и точка z от точки uАксиоматическое устройство геометрииАксиомы T1–T51). ∀x, y , z (B(x, y , z) → B(z, y , x))(аксиома симметричности предиката B)2). ∀x, y , z, u (B(x, y , u)&B(y , z, u) → B(x, y , z))(аксиома транзитивности предиката B)3). ∀x, y D(x, y , y , x)(аксиома симметричности равенства длин отрезков)4).