Презентация 16 (Лекции)

Математическая логикаи логическое программированиеЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2016, весенний семестрЧто ещё есть в логике?классическаялогикаЧто ещё есть в логике?аксиоматическиетеорииIклассическаялогикаI Специальные интерпретации логических формулЧто ещё есть в логике?логикивысших порядковIIаксиоматическиетеорииIклассическаялогикаI Специальные интерпретации логических формулII Более широкие возможности применения кванторовЧто ещё есть в логике?интуиционистскаялогикалогикивысших порядковIIIIIаксиоматическиетеорииIклассическаялогикаI Специальные интерпретации логических формулII Более широкие возможности применения кванторовIII Другая семантика логических операцийЧто ещё есть в логике?интуиционистскаятеориялогикадоказательствлогикивысших порядковIII IVIIаксиоматическиетеорииIIIIIIIVIклассическаялогикаСпециальные интерпретации логических формулБолее широкие возможности применения кванторовДругая семантика логических операцийДругие формы логического выводаЧто ещё есть в логике?интуиционистскаятеориялогикадоказательствлогикивысших порядковIIаксиоматическиетеорииIIIIIIIVVIмодальныелогикиIII IVVклассическаялогикаСпециальные интерпретации логических формулБолее широкие возможности применения кванторовДругая семантика логических операцийДругие формы логического выводаДругие логические операцииЧто ещё есть в логике?интуиционистскаятеориялогикадоказательствлогикивысших порядковIIаксиоматическиетеорииIIIIIIIVVVIIмодальныелогикиIII IVVклассическая VIлогикалогикав программированииСпециальные интерпретации логических формулБолее широкие возможности применения кванторовДругая семантика логических операцийДругие формы логического выводаДругие логические операцииЛогика в приложении к другим дисциплинам...Что ещё есть в логике?интуиционистскаятеориялогикадоказательствлогикивысших порядковIIаксиоматическиетеорииIIIIIIIVVVIIмодальныелогикиIII IVVклассическая VIлогикалогикав программированииСпециальные интерпретации логических формулБолее широкие возможности применения кванторовДругая семантика логических операцийДругие формы логического выводаДругие логические операцииЛогика в приложении к другим дисциплинам...Модальные логикиНачнём с примера:Зима близкоМодальные логикиНачнём с примера:1: Зима близко2: Зима всегда близкоМодальные логикиНачнём с примера:1: Зима близко2: Зима всегда близко3: Иногда зима близкоМодальные логикиНачнём с примера:1: Зима близко2: Зима всегда близко3: Иногда зима близкоЭти утверждения несут разный смысл, а значит, должны бытьописаны разными формуламиМодальные логикиНачнём с примера:1: Зима близко2: Зима всегда близко3: Иногда зима близкоЭти утверждения несут разный смысл, а значит, должны бытьописаны разными формуламиТем не менее утверждения связаны по смыслу, и эта взаимосвязьдолжна быть отражена в формулахМодальные логикиНачнём с примера:1: Зима близко2: Зима всегда близко3: Иногда зима близкоЭти утверждения несут разный смысл, а значит, должны бытьописаны разными формуламиТем не менее утверждения связаны по смыслу, и эта взаимосвязьдолжна быть отражена в формулахУтверждения отличаются только словами всегда и иногда (этомодальности времени)Модальные логикиНачнём с примера:1: Зима близко2: Зима всегда близко3: Иногда зима близкоЭти утверждения несут разный смысл, а значит, должны бытьописаны разными формуламиТем не менее утверждения связаны по смыслу, и эта взаимосвязьдолжна быть отражена в формулахУтверждения отличаются только словами всегда и иногда (этомодальности времени), а значит, достаточно ввести логическиеконструкции для этих модальностейМодальные логикиНачнём с примера:1: Зима близко2: Зима всегда близко3: Иногда зима близкоЭти утверждения несут разный смысл, а значит, должны бытьописаны разными формуламиТем не менее утверждения связаны по смыслу, и эта взаимосвязьдолжна быть отражена в формулахУтверждения отличаются только словами всегда и иногда (этомодальности времени), а значит, достаточно ввести логическиеконструкции для этих модальностейПодойдут ли для этих целей кванторы?Модальные логикиНачнём с примера:1: Зима близко2: Зима должна быть близко3: Зима имеет право быть близкоДолжен и имеет право — это деонтические модальностиМодальные логикиНачнём с примера:1: Зима близко2: Зима должна быть близко3: Зима имеет право быть близкоДолжен и имеет право — это деонтические модальностиА в этом случае можно использовать кванторы так же?Модальные логикиНачнём с примера:1: Зима близко2: Известно, что зима близко3: Можно допустить, что зима близкоИзвестно и допустимо — это эпистемологические модальностиМодальные логикиНачнём с примера:1: Зима близко2: Известно, что зима близко3: Можно допустить, что зима близкоИзвестно и допустимо — это эпистемологические модальностиА здесь?Модальные логикиМодальность — это выражение, описывающее “оттенокистинности” высказывания (уверенность, необходимость,доказуемость, осведомлённость, .

. . )Модальные логикиМодальность — это выражение, описывающее “оттенокистинности” высказывания (уверенность, необходимость,доказуемость, осведомлённость, . . . )Такие оттенки можно разбить на две категории:Модальность необходимого Модальность возможногоМодальные логикиМодальность — это выражение, описывающее “оттенокистинности” высказывания (уверенность, необходимость,доказуемость, осведомлённость, . .

. )Такие оттенки можно разбить на две категории:Модальность необходимого Модальность возможногонеобходимообязательновсегдадолжензнаетдоказуемоМодальные логикиМодальность — это выражение, описывающее “оттенокистинности” высказывания (уверенность, необходимость,доказуемость, осведомлённость, . . . )Такие оттенки можно разбить на две категории:Модальность необходимого Модальность возможногонеобходимовозможнообязательноне исключеновсегдаиногдадолженимеет правознаетпредполагаетдоказуемонепротиворечивоМодальные логикиМодальность — это выражение, описывающее “оттенокистинности” высказывания (уверенность, необходимость,доказуемость, осведомлённость, .

. . )Такие оттенки можно разбить на две категории:Модальность необходимого Модальность возможногонеобходимовозможнообязательноне исключеновсегдаиногдадолженимеет правознаетпредполагаетдоказуемонепротиворечиво23Модальные логикиСинтаксис модальных формулМодальные логикиСинтаксис модальных формулIНачнём с синтаксиса формул логики высказыванийМодальные логикиСинтаксис модальных формулIIНачнём с синтаксиса формул логики высказыванийДобавим к алфавиту модальные операторы (модальности):2, 3Модальные логикиСинтаксис модальных формулIIIНачнём с синтаксиса формул логики высказыванийДобавим к алфавиту модальные операторы (модальности):2, 3Добавим к синтаксису такое правило:I(2ϕ) и (3ϕ) — формулы(ϕ — формула)Модальные логикиСинтаксис модальных формулIIIНачнём с синтаксиса формул логики высказыванийДобавим к алфавиту модальные операторы (модальности):2, 3Добавим к синтаксису такое правило:II(2ϕ) и (3ϕ) — формулы(ϕ — формула)Считаем, что операторы 2, 3 имеют приоритет выше, чемлогические связки (¬, &, ∨, →)Модальные логикиСинтаксис модальных формулIIIНачнём с синтаксиса формул логики высказыванийДобавим к алфавиту модальные операторы (модальности):2, 3Добавим к синтаксису такое правило:II(2ϕ) и (3ϕ) — формулы(ϕ — формула)Считаем, что операторы 2, 3 имеют приоритет выше, чемлогические связки (¬, &, ∨, →)Модальности 2, 3 могут иметь совершенно разное значение собщим “оттенком” необходимости или возможностиМодальные логикиСинтаксис модальных формулIIIНачнём с синтаксиса формул логики высказыванийДобавим к алфавиту модальные операторы (модальности):2, 3Добавим к синтаксису такое правило:II(2ϕ) и (3ϕ) — формулы(ϕ — формула)Считаем, что операторы 2, 3 имеют приоритет выше, чемлогические связки (¬, &, ∨, →)Модальности 2, 3 могут иметь совершенно разное значение собщим “оттенком” необходимости или возможностиА как строго определить значение модальностей, чтобы приэтом охватить всевозможные оттенки?Модальные логикиПрежде чем перейти к описанию семантики модальных формул,рассмотрим такой пример:верна ли формула 2ϕ → ϕ?Модальные логикиПрежде чем перейти к описанию семантики модальных формул,рассмотрим такой пример:верна ли формула 2ϕ → ϕ?Да, если 2 — модальность времени:если зима всегда близко, то она близкоМодальные логикиПрежде чем перейти к описанию семантики модальных формул,рассмотрим такой пример:верна ли формула 2ϕ → ϕ?Да, если 2 — модальность времени:если зима всегда близко, то она близкоНет, если 2 — деонтическая модальность:если зима должна быть близко, то она близкоМодальные логикиПрежде чем перейти к описанию семантики модальных формул,рассмотрим такой пример:верна ли формула 2ϕ → ϕ?Да, если 2 — модальность времени:если зима всегда близко, то она близкоНет, если 2 — деонтическая модальность:если зима должна быть близко, то она близкоКак же учесть все трактовки 2, не основываясь на правдивостипрогноза погоды?Семантика Крипке— это наиболее распространённый способ описания значениямодальных формулСемантика Крипке— это наиболее распространённый способ описания значениямодальных формулПусть P — множество пропозициональных переменныхСемантика Крипке— это наиболее распространённый способ описания значениямодальных формулПусть P — множество пропозициональных переменныхТогда модель Крипке — это система (W , R, ξ), гдеIIIW — множество состояний (возможных миров)R ⊆ W × W — отношение достижимости мировξ : W → 2P — оценка переменныхСемантика Крипке— это наиболее распространённый способ описания значениямодальных формулПусть P — множество пропозициональных переменныхТогда модель Крипке — это система (W , R, ξ), гдеIIIW — множество состояний (возможных миров)R ⊆ W × W — отношение достижимости мировξ : W → 2P — оценка переменныхПара (W , R) образует шкалу Крипке(Kripke frame)Семантика Крипке— это наиболее распространённый способ описания значениямодальных формулПусть P — множество пропозициональных переменныхТогда модель Крипке — это система (W , R, ξ), гдеIIIW — множество состояний (возможных миров)R ⊆ W × W — отношение достижимости мировξ : W → 2P — оценка переменныхПара (W , R) образует шкалу Крипке(Kripke frame)w 0 — альтернативный мир для w , если (w , w 0 ) ∈ RСемантика Крипке— это наиболее распространённый способ описания значениямодальных формулПусть P — множество пропозициональных переменныхТогда модель Крипке — это система (W , R, ξ), гдеIIIW — множество состояний (возможных миров)R ⊆ W × W — отношение достижимости мировξ : W → 2P — оценка переменныхПара (W , R) образует шкалу Крипке(Kripke frame)w 0 — альтернативный мир для w , если (w , w 0 ) ∈ RМодель Крипке — это интерпретация модальных формулСемантика Крипке(P = {a})Например,w1w2w4w3w5— это шкала КрипкеСемантика Крипке(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель КрипкеСемантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)Семантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= p⇔p ∈ ξ(w )(p ∈ P)(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)Семантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= p⇔p ∈ ξ(w )(p ∈ P)(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)I, w1 |= a,I, w2 6|= aСемантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:IIII, w |= p ⇔ p ∈ ξ(w )I, w |= ϕ&ψ ⇔ I, w |= ϕ и I, w |= ψI, w |= ϕ ∨ ψ ⇔ I, w |= ϕ или I, w |= ψ(p ∈ P)(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)Семантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:III, w |= ϕ → ψ ⇔ I, w 6|= ϕ или I, w |= ψI, w |= ¬ϕ ⇔ I, w 6|= ϕ(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)Семантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= 2ϕ ⇔для любого альтернативного мира w 0 для wверно I, w 0 |= ϕ(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)Семантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= 2ϕ ⇔для любого альтернативного мира w 0 для wверно I, w 0 |= ϕ(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)I, w1 6|= 2aСемантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= 2ϕ ⇔для любого альтернативного мира w 0 для wверно I, w 0 |= ϕ(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)I, w1 6|= 2a,I, w5 |= 2aСемантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= 3ϕ ⇔существует альтернативный мир w 0 для w ,такой что верно I, w 0 |= ϕ(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)Семантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= 3ϕ ⇔существует альтернативный мир w 0 для w ,такой что верно I, w 0 |= ϕ(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)I, w1 |= 3aСемантика КрипкеОтношение выполнимости |= для модели I = (W , R, ξ) и мираw ∈ W определяется так:II, w |= 3ϕ ⇔существует альтернативный мир w 0 для w ,такой что верно I, w 0 |= ϕ(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5— это модель Крипке (I)I, w1 |= 3a,I, w5 6|= 3aСемантика Крипке(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5I, w1 |= 23a— это модель Крипке (I)Семантика Крипке(P = {a})Например,{a}w1∅w2w4∅w3{a}∅w5I, w1 |= 23a,— это модель Крипке (I)I, w5 |= 23aСемантика Крипке(P = {a})Например,{a}w1∅w2w4∅w3{a}I, w1 6|= 32a∅w5— это модель Крипке (I),Семантика Крипке(P = {a})Например,{a}w1∅w2w4∅w3{a}I, w1 6|= 32a,∅w5— это модель Крипке (I)I, w2 |= 32a,Семантика Крипке(P = {a})Например,{a}w1∅w2w4∅w3{a}I, w1 6|= 32a,∅w5— это модель Крипке (I)I, w2 |= 32a,I, w5 6|= 32aЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойстваЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Законы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыНапример, в эпистемической логике изучаются модальностизнания (2) и допущения (3) и причинно-следственные связимежду нимиЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыНапример, в эпистемической логике изучаются модальностизнания (2) и допущения (3) и причинно-следственные связимежду ними, и основные аксиомы этой логики:Iаксиома адекватности знания:2ϕ → ϕЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыНапример, в эпистемической логике изучаются модальностизнания (2) и допущения (3) и причинно-следственные связимежду ними, и основные аксиомы этой логики:Iаксиома адекватности знания:2ϕ → ϕ(мои знания верны)Законы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыНапример, в эпистемической логике изучаются модальностизнания (2) и допущения (3) и причинно-следственные связимежду ними, и основные аксиомы этой логики:IIаксиома адекватности знания:2ϕ → ϕаксиома позитивной интроспекции:2ϕ → 22ϕ(мои знания верны)Законы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыНапример, в эпистемической логике изучаются модальностизнания (2) и допущения (3) и причинно-следственные связимежду ними, и основные аксиомы этой логики:IIаксиома адекватности знания:(мои знания верны)2ϕ → ϕаксиома позитивной интроспекции:2ϕ → 22ϕ(мне известно, что именно я знаю)Законы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыНапример, в эпистемической логике изучаются модальностизнания (2) и допущения (3) и причинно-следственные связимежду ними, и основные аксиомы этой логики:IIIаксиома адекватности знания:(мои знания верны)2ϕ → ϕаксиома позитивной интроспекции:2ϕ → 22ϕ(мне известно, что именно я знаю)аксиома негативной интроспекции:¬2ϕ → 2¬2ϕЗаконы модальных логикЭпистемические логикиМодальная логика, как и любая другая, имеет свои законы исвойства, например:3ϕ ≈ ¬2¬ϕ |= ϕ ⇒ |= 2ϕ |= 2(ϕ → ψ) → (2ϕ → 2ψ)Смыслом модальностей могут определяться и другие законыНапример, в эпистемической логике изучаются модальностизнания (2) и допущения (3) и причинно-следственные связимежду ними, и основные аксиомы этой логики:IIIаксиома адекватности знания:(мои знания верны)2ϕ → ϕаксиома позитивной интроспекции:2ϕ → 22ϕ(мне известно, что именно я знаю)аксиома негативной интроспекции:¬2ϕ → 2¬2ϕ(мне известно, что я не знаю)Эпистемические логикиПример: задача о трёх мудрецахЭпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЭпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЗатем спросил: “Знаете ли вы, какая на вас шапка?”Эпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЗатем спросил: “Знаете ли вы, какая на вас шапка?”“Нет, не знаем”, хором ответили мудрецыЭпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЗатем спросил: “Знаете ли вы, какая на вас шапка?”“Нет, не знаем”, хором ответили мудрецыОн задал тот же вопрос второй разЭпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЗатем спросил: “Знаете ли вы, какая на вас шапка?”“Нет, не знаем”, хором ответили мудрецыОн задал тот же вопрос второй раз“Нет, не знаем”, хором ответили мудрецыЭпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЗатем спросил: “Знаете ли вы, какая на вас шапка?”“Нет, не знаем”, хором ответили мудрецыОн задал тот же вопрос второй раз“Нет, не знаем”, хором ответили мудрецыОн спросил то же в третий разЭпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЗатем спросил: “Знаете ли вы, какая на вас шапка?”“Нет, не знаем”, хором ответили мудрецыОн задал тот же вопрос второй раз“Нет, не знаем”, хором ответили мудрецыОн спросил то же в третий раз“Да, чёрная”, хором ответили мудрецыЭпистемические логикиПример: задача о трёх мудрецахКороль призвал трёх мудрецов и, чтобы убедиться в ихмудрости, придумал такое испытание: показал им три чёрныешапки и две белые, завязал глаза, надел на каждого чёрнуюшапку и развязал глазаЗатем спросил: “Знаете ли вы, какая на вас шапка?”“Нет, не знаем”, хором ответили мудрецыОн задал тот же вопрос второй раз“Нет, не знаем”, хором ответили мудрецыОн спросил то же в третий раз“Да, чёрная”, хором ответили мудрецыА как строго описать ход рассуждений мудрецов с помощьюэпистемической логики?Темпоральные логикиТемпоральные (временные) логики основываются намодальной логике и применяются для исследованиявзаимосвязи событий, развивающихся во времениТемпоральные логикиТемпоральные (временные) логики основываются намодальной логике и применяются для исследованиявзаимосвязи событий, развивающихся во времени2 = G = “всегда”,3 = F = “когда-нибудь”Темпоральные логикиТемпоральные (временные) логики основываются намодальной логике и применяются для исследованиявзаимосвязи событий, развивающихся во времени2 = G = “всегда”,3 = F = “когда-нибудь”Значение формул темпоральных логик зависит от того, какописывается феномен времени, то есть от того, какая шкалавыбрана для описания развития времениТемпоральные логикиТемпоральные (временные) логики основываются намодальной логике и применяются для исследованиявзаимосвязи событий, развивающихся во времени2 = G = “всегда”,3 = F = “когда-нибудь”Значение формул темпоральных логик зависит от того, какописывается феномен времени, то есть от того, какая шкалавыбрана для описания развития времениСамые известные темпоральные логики:ILTL (Linear Temporal Logic)ICTL (Computation Tree Logic)Темпоральные логикиТемпоральные (временные) логики основываются намодальной логике и применяются для исследованиявзаимосвязи событий, развивающихся во времени2 = G = “всегда”,3 = F = “когда-нибудь”Значение формул темпоральных логик зависит от того, какописывается феномен времени, то есть от того, какая шкалавыбрана для описания развития времениСамые известные темпоральные логики:IILTL (Linear Temporal Logic): время линейно, свойство(формула) проверяется для каждого развития событийCTL (Computation Tree Logic)Темпоральные логикиТемпоральные (временные) логики основываются намодальной логике и применяются для исследованиявзаимосвязи событий, развивающихся во времени2 = G = “всегда”,3 = F = “когда-нибудь”Значение формул темпоральных логик зависит от того, какописывается феномен времени, то есть от того, какая шкалавыбрана для описания развития времениСамые известные темпоральные логики:IILTL (Linear Temporal Logic): время линейно, свойство(формула) проверяется для каждого развития событийCTL (Computation Tree Logic): время — это частичноупорядоченное множество, в каждый момент происходитвыбор альтернативы развития событий, свойствапроверяются для всевозможных альтернативТемпоральные логикиЛогика линейного времени (LTL)Шкала Крипке для LTL — это естественно упорядоченныйнатуральный ряд:12345...Темпоральные логикиЛогика линейного времени (LTL)Шкала Крипке для LTL — это естественно упорядоченныйнатуральный ряд:I:1p, ¬q2p, q3p, ¬q4p, ¬q5p, ¬q...Темпоральные логикиЛогика линейного времени (LTL)Шкала Крипке для LTL — это естественно упорядоченныйнатуральный ряд:I:1p, ¬q2p, q3p, ¬q4p, ¬qI, 1 |= Gp5p, ¬q...Темпоральные логикиЛогика линейного времени (LTL)Шкала Крипке для LTL — это естественно упорядоченныйнатуральный ряд:I:1p, ¬q2p, q3p, ¬q4p, ¬qI, 1 |= GpI, 1 6|= Gq5p, ¬q...Темпоральные логикиЛогика линейного времени (LTL)Шкала Крипке для LTL — это естественно упорядоченныйнатуральный ряд:I:1p, ¬q2p, q3p, ¬q4p, ¬qI, 1 |= GpI, 1 6|= GqI, 1 |= Fq5p, ¬q...Темпоральные логикиЛогика линейного времени (LTL)Шкала Крипке для LTL — это естественно упорядоченныйнатуральный ряд:I:1p, ¬q2p, q3p, ¬q4p, ¬qI, 1 |= GpI, 1 6|= GqI, 1 |= FqI, 1 6|= GFq5p, ¬q...Темпоральные логикиЛогика линейного времени (LTL)Шкала Крипке для LTL — это естественно упорядоченныйнатуральный ряд:I:1p, ¬q2p, q3p, ¬q4p, ¬q5p, ¬q...I, 1 |= GpI, 1 6|= GqI, 1 |= FqI, 1 6|= GFqПодробнее об LTL будет рассказано на следующих лекцияхТемпоральные логикиЛогика деревьев вычислений (CTL)Шкала Крипке для CTL — это (бесконечное) деревоТемпоральные логикиЛогика деревьев вычислений (CTL)Шкала Крипке для CTL — это (бесконечное) дерево(точнее, его рефлексивно-транзитивное замыкание)Темпоральные логикиЛогика деревьев вычислений (CTL)Шкала Крипке для CTL — это (бесконечное) дерево(точнее, его рефлексивно-транзитивное замыкание)Темпоральные операторы CTL подразделяются науниверсальные (AG, AF) и экзистенциальные (EG, EF):Темпоральные логикиЛогика деревьев вычислений (CTL)Шкала Крипке для CTL — это (бесконечное) дерево(точнее, его рефлексивно-транзитивное замыкание)Темпоральные операторы CTL подразделяются науниверсальные (AG, AF) и экзистенциальные (EG, EF):II, v |= AGϕ ⇔для каждой вершины v 0 , достижимой из v , верно I, v 0 |= ϕТемпоральные логикиЛогика деревьев вычислений (CTL)Шкала Крипке для CTL — это (бесконечное) дерево(точнее, его рефлексивно-транзитивное замыкание)Темпоральные операторы CTL подразделяются науниверсальные (AG, AF) и экзистенциальные (EG, EF):III, v |= AGϕ ⇔для каждой вершины v 0 , достижимой из v , верно I, v 0 |= ϕI, v |= AFϕ ⇔в каждой ветви, исходящей из v , существует вершина v 0 ,такая что I, v 0 |= ϕТемпоральные логикиЛогика деревьев вычислений (CTL)Шкала Крипке для CTL — это (бесконечное) дерево(точнее, его рефлексивно-транзитивное замыкание)Темпоральные операторы CTL подразделяются науниверсальные (AG, AF) и экзистенциальные (EG, EF):IIII, v |= AGϕ ⇔для каждой вершины v 0 , достижимой из v , верно I, v 0 |= ϕI, v |= AFϕ ⇔в каждой ветви, исходящей из v , существует вершина v 0 ,такая что I, v 0 |= ϕI, v |= EGϕ ⇔существует ветвь, исходящая из v , такая что для всех еёвершин v 0 верно I, v 0 |= ϕТемпоральные логикиЛогика деревьев вычислений (CTL)Шкала Крипке для CTL — это (бесконечное) дерево(точнее, его рефлексивно-транзитивное замыкание)Темпоральные операторы CTL подразделяются науниверсальные (AG, AF) и экзистенциальные (EG, EF):IIIII, v |= AGϕ ⇔для каждой вершины v 0 , достижимой из v , верно I, v 0 |= ϕI, v |= AFϕ ⇔в каждой ветви, исходящей из v , существует вершина v 0 ,такая что I, v 0 |= ϕI, v |= EGϕ ⇔существует ветвь, исходящая из v , такая что для всех еёвершин v 0 верно I, v 0 |= ϕI, v |= EFϕ ⇔из v достижима вершина v 0 , такая что I, v 0 |= ϕТемпоральные логикиПример:Темпоральные логикиПример:I,|= AG ppI:pppppppppppТемпоральные логикиПример:I,I:|= EG pppppТемпоральные логикиПример:I,|= AF pI:ppppТемпоральные логикиПример:I,|= EF pI:pТемпоральные логикиА какие высказывания выразимы формулами логики CTL?Темпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,Iможет производиться перезапуск(переменная restart)Темпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,IIможет производиться перезапускможет посылаться запрос(переменная restart)(переменная request)Темпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,IIIможет производиться перезапуск(переменная restart)может посылаться запрос(переменная request)на запрос может быть получен отклик(переменная response)Темпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,IIIможет производиться перезапуск(переменная restart)может посылаться запрос(переменная request)на запрос может быть получен отклик(переменная response)Тогда в логике CTL выразимы, например, такие свойства:Iкак бы ни работала система, её можно перезапуститьТемпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,IIIможет производиться перезапуск(переменная restart)может посылаться запрос(переменная request)на запрос может быть получен отклик(переменная response)Тогда в логике CTL выразимы, например, такие свойства:Iкак бы ни работала система, её можно перезапуститьAG EF restartТемпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,IIIможет производиться перезапуск(переменная restart)может посылаться запрос(переменная request)на запрос может быть получен отклик(переменная response)Тогда в логике CTL выразимы, например, такие свойства:IIкак бы ни работала система, её можно перезапуститьAG EF restartна любой запрос рано или поздно будет получен откликТемпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,IIIможет производиться перезапуск(переменная restart)может посылаться запрос(переменная request)на запрос может быть получен отклик(переменная response)Тогда в логике CTL выразимы, например, такие свойства:IIкак бы ни работала система, её можно перезапуститьAG EF restartна любой запрос рано или поздно будет получен откликAG (request → AF response)Темпоральные логикиА какие высказывания выразимы формулами логики CTL?Например, представим себе систему, работающую в реальномвремени, в которой, в числе прочего,IIIможет производиться перезапуск(переменная restart)может посылаться запрос(переменная request)на запрос может быть получен отклик(переменная response)Тогда в логике CTL выразимы, например, такие свойства:IIкак бы ни работала система, её можно перезапуститьAG EF restartна любой запрос рано или поздно будет получен откликAG (request → AF response)А насколько важно и трудно проверять подобные свойства?Формальная верификацияФормальная верификация“Любая нетривиальная программасодержит хотя бы одну ошибку”автор неизвестенФормальная верификация“Любая нетривиальная программасодержит хотя бы одну ошибку”автор неизвестенПравильная программа ошибок не содержитФормальная верификация“Любая нетривиальная программасодержит хотя бы одну ошибку”автор неизвестенПравильная программа ошибок не содержитА как проверить, что программа не содержит ошибок?Формальная верификация“Любая нетривиальная программасодержит хотя бы одну ошибку”автор неизвестенПравильная программа ошибок не содержитА как проверить, что программа не содержит ошибок?Программа без ошибок работает в точности так, как от неётребуетсяФормальная верификация“Любая нетривиальная программасодержит хотя бы одну ошибку”автор неизвестенПравильная программа ошибок не содержитА как проверить, что программа не содержит ошибок?Программа без ошибок работает в точности так, как от неётребуетсяА как убедиться, что программа делает в точности то, что отнеё требуется?Формальная верификация“Любая нетривиальная программасодержит хотя бы одну ошибку”автор неизвестенПравильная программа ошибок не содержитА как проверить, что программа не содержит ошибок?Программа без ошибок работает в точности так, как от неётребуетсяА как убедиться, что программа делает в точности то, что отнеё требуется?Для этого надо:1.