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

Семантика правила вывода такова: если истиннымпредпосылки, то истинно и заключения.Определение. Правилом вывода называется фигура следующего вида:Рассмотрим следующую систему правил:ϕ → ϕ '1 ,{ϕ '1} < Π > {ϕ '2 }, ϕ 2 → ϕ '2(ослабления)1. 1{ϕ1} < Π > {ϕ 2 }2.{ }ϕ →ψ x t(присваивания){ϕ} < x:= t > {ψ }{ϕ} < Π1 > {χ },{χ } < Π 2 > {ψ }3.(последовательного соединения){ϕ} < Π1 ; Π 2 > {ψ }{ϕ & A} < Π1 > {ψ },{ϕ & ¬A} < Π 2 > {ψ }4.(ветвления){ϕ & A} < if_A_then_Π1_else_Π 2 _fi > {ψ }23Математическая логика, сводка определений.

(с) 2006 GrGr (grgr@later.ru){χ inv & A} < Π >, χ inv & ¬A → ψ , ϕ → χ inv(итерации; χ inv называется инвариантом{ϕ} < while_A_do_Π > {ψ }оператора итерации, для проверки правильности работы цикла требуется его найти)6. {ϕ} < eps > {ϕ } (аксиома)5.Система таких правил называется PVS (Prototype Verification System) и позволяет упрощатьпроверку правильности программ.4.4.

Логики знанийРассмотрим мультиагентную систему (сложную систему, принимающую решения)A1 , A2 ,..., An программ-агентов. При этом принятие решения может опираться на то, чтознают или не знают другие участники процесса принятия решений.Определение. Модальным оператором называется оператор , который выражаетотношение уверенности (необходимости).

Его семантика такова:яϕ означает «я знаю, что формула ϕ истинна».Вопрос общезначимости формулыϕ → ϕ - вопрос непротиворечивости базы знаний.яВопрос общезначимости формулы ϕ →ϕ - вопрос полноты базы знаний.я4.5. Динамическая логика (логика программ)Синтаксис динамической логики состоит из двух частей:ПрограммыФормулыA = {a1 , a2 ,..., an } - набор базовых действийP = {ϕ1 , ϕ2 ,..., ϕn } - набор базовых условий(операторов)(пропозиционных переменных)1) a ∈ A - программа;1) ϕ ∈ P - формула;2) Π1 , Π 2 - программа;2) ϕ1 & ϕ2 , ϕ1 ∨ ϕ2 , ϕ1 → ϕ2 , ¬ ϕ - формулы;3) Π1 || Π 2 - программа (|| 3) если П – программа, то [Π ]ϕ - формула.недетермированный выбор);4) (Π i ) * - программа;5) ϕ ? - программа (тест; ϕ - формула).Пример: выражение {ϕ } <if A then П1 else П2 fi > {ψ } , записанное в терминах логикиХоара, в терминах динамической логики будет выглядеть как ϕ → [( A ?, Π1 ) + (¬A ?, Π 2 )]ψ .24.