Динамическая логика (модальная логика)

Динамическая логика - это расширение модальной логики, изначально предназначенной для рассуждений о компьютерных программах, а затем примененной к более общим сложным формам поведения, возникающим в лингвистике , философии , искусственном интеллекте и других областях.

Язык [ править ]

Модальная логика характеризуется модальными операторами (рамка p), утверждающими, что это обязательно так, и (ромб p), утверждающими, что , возможно, так. Динамическая логика расширяет это, связывая с каждым действием модальные операторы и тем самым делая его мультимодальной логикой . Смысл в том, что после совершения действия обязательно имеет место, то есть должно произойти . Смысл в том, что после выполнения возможно, что удержание, то есть может вызвать . Эти операторы связаны между собой и${\ displaystyle \ Box p}$${\ Displaystyle р \, \!}$${\ displaystyle \ Diamond p}$${\ Displaystyle р \, \!}$${\ Displaystyle а \, \!}$${\ Displaystyle [а] \, \!}$${\ Displaystyle \ langle а \ rangle \, \!}$${\ Displaystyle [а] п \, \!}$${\ Displaystyle а \, \!}$${\ Displaystyle р \, \!}$${\ Displaystyle а \, \!}$${\ Displaystyle р \, \!}$${\ displaystyle \ langle a \ rangle p \, \!}$${\ Displaystyle а \, \!}$${\ Displaystyle р \, \!}$${\ Displaystyle а \, \!}$${\ Displaystyle р \, \!}$${\displaystyle [a]p\equiv \neg \langle a\rangle \neg p\,\!}$${\displaystyle \langle a\rangle p\equiv \neg [a]\neg p\,\!}$, аналогично соотношению между кванторами универсального ( ) и экзистенциального ( ).${\displaystyle \forall \,\!}$${\displaystyle \exists \,\!}$

Динамическая логика позволяет создавать сложные действия из более мелких. В то время как основные операторы управления любого языка программирования можно были бы использовать для этой цели, Клини «s регулярные выражения операторы хорошо соответствуют модальной логике. Данные действия и , составное действие , выбор , также записанное или , выполняется путем выполнения одного из или . Сложное действие , последовательность , выполняется сначала, а затем . Составное действие , итерация , выполняется путем последовательного выполнения нуля или более раз. Постоянное действие или${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle a\cup b\,\!}$${\displaystyle a+b\,\!}$${\displaystyle a|b\,\!}$${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle a{\mathbin {;}}b\,\!}$${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle a{*}\,\!}$${\displaystyle a\,\!}$${\displaystyle 0\,\!}$BLOCK ничего не делает и не завершается, тогда как постоянное действие или SKIP или NOP , определяемое как , ничего не делает, а завершается.${\displaystyle 1\,\!}$${\displaystyle 0{*}\,\!}$

Аксиомы [ править ]

Эти операторы могут быть аксиоматизированы в динамической логике следующим образом, принимая как уже заданную подходящую аксиоматизацию модальной логики, включая такие аксиомы для модальных операторов, как упомянутая выше аксиома и два правила вывода: modus ponens ( и подразумевает ) и необходимость ( подразумевает ).${\displaystyle [a]p\equiv \neg \langle a\rangle \neg p\,\!}$${\displaystyle \vdash p}$${\displaystyle \vdash p\to q}$${\displaystyle \vdash q\,}$${\displaystyle \vdash p}$${\displaystyle \vdash [a]p\,}$

А1. ${\displaystyle [0]p\,\!}$

A2. ${\displaystyle [1]p\equiv p\,\!}$

A3. ${\displaystyle [a\cup b]p\equiv [a]p\land [b]p\,\!}$

A4. ${\displaystyle [a{\mathbin {;}}b]p\equiv [a][b]p\,\!}$

А5. ${\displaystyle [a*]p\equiv p\land [a][a*]p\,\!}$

А6. ${\displaystyle p\land [a*](p\to [a]p)\to [a*]p\,\!}$

Аксиома A1 дает пустое обещание, что после завершения BLOCK будет выполнено, даже если предложение является ложным . (Таким образом, BLOCK абстрагирует сущность действия замораживания ада.) A2 говорит, что NOP действует как функция тождества в предложениях, то есть он трансформируется в себя. A3 говорит, что если выполнение одного из или должно вызывать , то должно вызывать и то же самое , и наоборот. A4 говорит, что если действие и затем должно вызвать , то должно вызвать ситуацию, в которой должно произойти .${\displaystyle p\,\!}$${\displaystyle p\,\!}$
${\displaystyle p\,\!}$
${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle p\,\!}$${\displaystyle b\,\!}$
${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle p\,\!}$
А5 является очевидным результатом применения А2, А3 и А4 к уравнению из клиниевской алгебры . А6 утверждает, что если выполняется сейчас, и независимо от того, как часто мы выполняем, остается таковым, что истинность после этого выполнения влечет за собой его истинность после еще одного выполнения , то должно оставаться верным независимо от того, как часто мы выполняем . A6 можно распознать как математическую индукцию с действием n: = n + 1 увеличения n, обобщенного на произвольные действия .${\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!}$
${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle a\,\!}$

Производные [ править ]

Аксиома модальной логики позволяет вывести следующие шесть теорем, соответствующих вышеизложенному:${\displaystyle [a]p\equiv \neg \langle a\rangle \neg p\,\!}$

Т1. ${\displaystyle \neg \langle 0\rangle p\,\!}$

Т2. ${\displaystyle \langle 1\rangle p\equiv p\,\!}$

Т3. ${\displaystyle \langle a\cup b\rangle p\equiv \langle a\rangle p\lor \langle b\rangle p\,\!}$

Т4. ${\displaystyle \langle a;b\rangle p\equiv \langle a\rangle \langle b\rangle p\,\!}$

Т5. ${\displaystyle \langle a*\rangle p\equiv p\lor \langle a\rangle \langle a*\rangle p\,\!}$

Т6. ${\displaystyle \langle a*\rangle p\to p\lor \langle a*\rangle (\neg p\land \langle a\rangle p)\,\!}$

T1 заявляет о невозможности чего-либо добиться, выполняя BLOCK .
T2 снова отмечает, что NOP ничего не меняет, имея в виду, что NOP и детерминирован, и завершается откуда и имеет одинаковую силу. T3 говорит, что если выбор или может привести , то либо либо, либо в одиночку, может привести . Т4 такой же, как А4. T5 объясняется как для A5. T6 утверждает, что если можно добиться , выполняя достаточно часто, то либо верно сейчас, либо можно выполнять неоднократно, чтобы вызвать ситуацию, когда${\displaystyle [1]\,\!}$${\displaystyle \langle 1\rangle \,\!}$
${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle b\,\!}$${\displaystyle p\,\!}$


${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle p\,\!}$(все еще) ложно, но может произойти еще одно исполнение .${\displaystyle a\,\!}$${\displaystyle p\,\!}$

Коробка и ромб полностью симметричны по отношению к примитиву. Альтернативной аксиоматизацией было бы принять теоремы T1-T6 в качестве аксиом, из которых мы могли бы затем вывести A1-A6 в качестве теорем.

Разница между импликацией и умозаключением в динамической логике такая же, как и в любой другой логике: тогда как импликация утверждает, что если истинно, то так и есть , а умозаключение утверждает, что если действительно, то так и есть . Однако динамический характер динамической логики перемещает это различие из области абстрактной аксиоматики в обыденный опыт постоянно меняющихся ситуаций. Правило вывода , например, является правильным, потому что его предпосылка утверждает, что оно выполняется всегда, откуда бы мы ни вели нас, там будет истинным. Однако импликация недействительна, потому что истинность в настоящий момент не является гарантией ее истинности после выполнения${\displaystyle p\to q\,\!}$${\displaystyle p\,\!}$${\displaystyle q\,\!}$${\displaystyle p\vdash q\,\!}$${\displaystyle p\,\!}$${\displaystyle q\,\!}$${\displaystyle p\vdash [a]p\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$${\displaystyle p\,\!}$${\displaystyle p\to [a]p\,\!}$${\displaystyle p\,\!}$${\displaystyle a\,\!}$. Например, будет истинным в любой ситуации, когда ложно, или в любой ситуации, когда истинно, но утверждение ложно в любой ситуации, когда имеет значение 1 и, следовательно, недействительно.${\displaystyle p\to [a]p\,\!}$${\displaystyle p\,\!}$${\displaystyle [a]p\,\!}$${\displaystyle (x=1)\to [x:=x+1](x=1)\,\!}$${\displaystyle x\,\!}$

Производные правила вывода [ править ]

Что касается модальной логики, то правила вывода modus ponens и необходимости также достаточны для динамической логики как единственные необходимые ей примитивные правила, как отмечалось выше. Однако, как обычно в логике, с помощью аксиом из них можно вывести гораздо больше правил. Примером такого производного правила в динамической логике является то, что если один раз ударить сломанный телевизор ногой невозможно, то его нельзя исправить, то неоднократные удары ногой тоже не могут его исправить. Написание для действия удара ногой по телевизору и для утверждения о том, что телевизор сломан, динамическая логика выражает этот вывод как , имея как предпосылку, так и заключение . Смысл в том, что гарантировано, что после удара по телевизору он сломается. Отсюда посылка${\displaystyle k\,\!}$${\displaystyle b\,\!}$${\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}$${\displaystyle b\to [k]b\,\!}$${\displaystyle b\to [k*]b\,\!}$${\displaystyle [k]b\,\!}$${\displaystyle b\to [k]b\,\!}$означает, что если телевизор сломается, то после одного удара ногой он все равно сломается. обозначает действие удара ногой по телевизору ноль или более раз. Отсюда следует вывод, что если телевизор сломан, то после ноль или более ударов ногами он все равно сломается. Ведь если нет, то после предпоследнего удара телевизор окажется в состоянии, когда повторный удар по нему все исправит, что, как утверждает предпосылка, не может произойти ни при каких обстоятельствах.${\displaystyle k{*}\,\!}$${\displaystyle b\to [k*]b\,\!}$

Вывод верен. Однако импликация неверна, потому что мы можем легко найти ситуации, в которых выполняется, но не выполняется. В любой такой контрпримерной ситуации должно выполняться, но должно быть ложным, но должно быть истинным. Но это могло произойти в любой ситуации, когда телевизор сломался, но его можно оживить двумя ударами. Импликация терпит неудачу (недействительна), потому что она требует этого удержания только сейчас, тогда как вывод успешен (является правильным), потому что он требует этого удержания во всех ситуациях, а не только в текущей.${\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}$${\displaystyle (b\to [k]b)\to (b\to [k*]b)\,\!}$${\displaystyle b\to [k]b\,\!}$${\displaystyle b\to [k*]b\,\!}$${\displaystyle b\,\!}$${\displaystyle [k*]b\,\!}$${\displaystyle [k]b\,\!}$${\displaystyle b\to [k]b\,\!}$${\displaystyle b\to [k]b\,\!}$

Пример правильного импликации - это предложение . Это говорит о том, что , если больше или равно 3, то после увеличения , должно быть больше или равно 4. В случае детерминированных действий , которые гарантированно прекратить, например , сусло и может иметь ту же силу, что есть, и имеют то же значение. Таким образом, выше предположение эквивалентно утверждать , что , если больше или равно 3 , то после выполнения , может быть больше или равно 4.${\displaystyle (x\geq 3)\to [x:=x+1](x\geq 4)\,\!}$${\displaystyle x\,\!}$${\displaystyle x\,\!}$${\displaystyle x\,\!}$${\displaystyle a\,\!}$${\displaystyle x:=x+1\,\!}$${\displaystyle [a]\,\!}$${\displaystyle \langle a\rangle \,\!}$${\displaystyle (x\geq 3)\to \langle x:=x+1\rangle (x\geq 4)\,\!}$${\displaystyle x\,\!}$${\displaystyle x:=x+1\,\!}$${\displaystyle x\,\!}$

Назначение [ править ]

Общая форма оператора присваивания - это где - переменная, а это выражение, построенное из констант и переменных с любыми операциями, предоставляемыми языком, такими как сложение и умножение. Аксиома Хоара для присваивания не дана как отдельная аксиома, а скорее как схема аксиом.${\displaystyle x:=e\,\!}$${\displaystyle x\,\!}$${\displaystyle e\,\!}$

А7. ${\displaystyle [x:=e]\Phi (x)\equiv \Phi (e)\,\!}$

Это схема в том смысле, что ее можно создать с помощью любой формулы, содержащей ноль или более экземпляров переменной . Значение заключается в тех вхождениях, которые встречаются свободно в , т. Е. Не связаны каким-либо квантификатором, например , заменяется на . Например, мы можем создать экземпляр A7 с помощью или с помощью . Такая схема аксиом позволяет записать бесконечное количество аксиом, имеющих общую форму, в виде конечного выражения, обозначающего эту форму.${\displaystyle \Phi (x)\,\!}$${\displaystyle \Phi \,\!}$${\displaystyle x\,\!}$${\displaystyle \Phi (e)\,\!}$${\displaystyle \Phi \,\!}$${\displaystyle x\,\!}$${\displaystyle \Phi \,\!}$${\displaystyle \forall x\,\!}$${\displaystyle e\,\!}$${\displaystyle [x:=e](x=y^{2})\equiv e=y^{2}\,\!}$${\displaystyle [x:=e](b=c+x)\equiv b=c+e\,\!}$

Экземпляр А7 позволяет рассчитать механически , что пример встречается несколько абзацев назад эквивалентно , в свою очередь , эквивалентно по элементарной алгебре .${\displaystyle [x:=x+1](x\geq 4)\equiv (x+1)\geq 4\,\!}$${\displaystyle [x:=x+1]x\geq 4\,\!}$${\displaystyle (x+1)\geq 4\,\!}$${\displaystyle x\geq 3\,\!}$

Примером, иллюстрирующим назначение в сочетании с, является предложение . Это утверждает, что можно путем достаточно частого приращения сделать равным 7. Это, конечно, не всегда верно, например, если 8 для начала или 6.5, поэтому это утверждение не является теоремой динамической логики. Однако если имеет целочисленный тип, то это утверждение верно тогда и только тогда, когда для начала не более 7, то есть это просто окольный способ выражения .${\displaystyle *\,\!}$${\displaystyle \langle (x:=x+1)*\rangle x=7\,\!}$${\displaystyle x\,\!}$${\displaystyle x\,\!}$${\displaystyle x\,\!}$${\displaystyle x\,\!}$${\displaystyle x\,\!}$${\displaystyle x\leq 7\,\!}$

Математическая индукция может быть получена как пример A6, в котором предложение реализуется как , действие as и as . Первые два из этих трех экземпляров просты и преобразуют A6 в . Однако якобы простая замена for не так проста, поскольку она выявляет так называемую ссылочную непрозрачность модальной логики в том случае, когда модальность может мешать замене.${\displaystyle p\,\!}$${\displaystyle \Phi (n)\,\!}$${\displaystyle a\,\!}$${\displaystyle n:=n+1\,\!}$${\displaystyle n\,\!}$${\displaystyle 0\,\!}$${\displaystyle (\Phi (n)\land [(n:=n+1)*](\Phi (n)\to [n:=n+1]\Phi (n)))\to [(n:=n+1)*]\Phi (n)\,\!}$${\displaystyle 0\,\!}$${\displaystyle n\,\!}$

Когда мы заменили на , мы думали о символе пропозиции в качестве жесткого целеуказателя по отношению к модальности , а это означает , что одно и то же предложение после приращения , как и раньше, несмотря на то, увеличивающиеся может повлиять на его истинность. Точно так же действие остается тем же действием после увеличения , даже если увеличение приведет к его выполнению в другой среде. Однако сам по себе не является жестким обозначением в отношении модальности ; если он обозначает 3 до увеличения , это означает 4 после. Таким образом , мы не можем просто заменить на повсюду в A6.${\displaystyle \Phi (n)\,\!}$${\displaystyle p\,\!}$${\displaystyle p\,\!}$${\displaystyle [n:=n+1]\,\!}$${\displaystyle n\,\!}$${\displaystyle n\,\!}$${\displaystyle a\,\!}$${\displaystyle n\,\!}$${\displaystyle n\,\!}$${\displaystyle n\,\!}$${\displaystyle [n:=n+1]\,\!}$${\displaystyle n\,\!}$${\displaystyle 0\,\!}$${\displaystyle n\,\!}$

Один из способов справиться с непрозрачностью модальностей - устранить их. С этой целью расширить как бесконечное вместе , то есть, в сочетании над всеми из . Теперь примените A4, чтобы превратить в , имея модальности. Затем примените к нему время аксиомы Хоара, чтобы получить , а затем упростите это бесконечное соединение до . Все это сокращение должно применяться к обоим экземплярам в A6, уступая . Оставшаяся модальность теперь может быть устранена еще одним использованием аксиомы Хоара .${\displaystyle [(n:=n+1)*]\Phi (n)\,\!}$${\displaystyle [(n:=n+1)^{0}]\Phi (n)\land [(n:=n+1)^{1}]\Phi (n)\land [(n:=n+1)^{2}]\Phi (n)\land \ldots \,\!}$${\displaystyle i\,\!}$${\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}$${\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}$${\displaystyle [n:=n+1][n:=n+1]\ldots \Phi (n)\,\!}$${\displaystyle i\,\!}$${\displaystyle i\,\!}$${\displaystyle \Phi (n+i)\,\!}$${\displaystyle \forall i\Phi (n+i)\,\!}$${\displaystyle [(n:=n+1)*]\,\!}$${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to [n:=n+1]\Phi (n+i)))\to \forall i\Phi (n+i)\,\!}$${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}$

С непрозрачных модальностей теперь из пути, можно смело заменить на в обычной манере логики первого порядка , чтобы получить Пеано знаменитую аксиому «s , а именно математической индукции.${\displaystyle 0\,\!}$${\displaystyle n\,\!}$${\displaystyle (\Phi (0)\land \forall i(\Phi (i)\to \Phi (i+1)))\to \forall i\Phi (i)\,\!}$

Одна тонкость, которую мы здесь упустили, заключается в том, что ее следует понимать как переход по натуральным числам, где - верхний индекс в разложении как объединение всех натуральных чисел . Важность сохранения этой типизированной информации становится очевидной, если бы она была целочисленной или даже реальной , для любого из которых A6 совершенно справедливо в качестве аксиомы. В качестве примера, если - действительная переменная, а предикат - натуральное число , то аксиома A6 после первых двух замен, то есть, так же действительна, то есть истинна в каждом состоянии независимо от значения в том состоянии, как когда он типа${\displaystyle \forall i\,\!}$${\displaystyle i\,\!}$${\displaystyle a{*}\,\!}$${\displaystyle a^{i}\,\!}$${\displaystyle i\,\!}$${\displaystyle n\,\!}$${\displaystyle n\,\!}$${\displaystyle \Phi (n)\,\!}$${\displaystyle n\,\!}$ ${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}$${\displaystyle n\,\!}$${\displaystyle n\,\!}$натуральное число . Если в данном состоянии находится натуральное число, то антецедент основного импликации A6 выполняется, но тогда также является натуральным числом, так что консеквент также имеет место. Если не является натуральным числом, то антецедент ложен, и поэтому A6 остается верным независимо от истинности консеквента. Мы могли бы усилить A6 до эквивалентности, не влияя ни на что из этого. Другое направление доказуемо из A5, из которого мы видим, что если антецедент A6 действительно где-то ложен, то консеквент должен быть ложным.${\displaystyle n\,\!}$${\displaystyle n+i\,\!}$${\displaystyle n\,\!}$${\displaystyle p\land [a*](p\to [a]p)\equiv [a*]p\,\!}$

Тест [ править ]

Динамическая логика связывает каждое предложение с действием, называемым тестом. Когда удерживается, тест действует как NOP , ничего не меняя, позволяя действию продолжить. Когда ложно, действует как БЛОК . Аксиоматизировать тесты можно следующим образом.${\displaystyle p\,\!}$${\displaystyle p?\,\!}$${\displaystyle p\,\!}$${\displaystyle p?\,\!}$${\displaystyle p\,\!}$${\displaystyle p?\,\!}$

А8. ${\displaystyle [p?]q\equiv p\to q\,\!}$

Соответствующая теорема для :${\displaystyle \langle p?\rangle \,\!}$

Т8. ${\displaystyle \langle p?\rangle q\equiv p\land q\,\!}$

Конструкция if p then a else b реализуется в динамической логике как . Это действие выражает защищенный выбор: если hold, то эквивалентно , тогда как эквивалентно BLOCK и эквивалентно . Следовательно, когда истинно, исполнитель действия может взять только левую ветвь, а когда ложно - правую.${\displaystyle (p?;a)\cup (\neg p?;b)\,\!}$${\displaystyle p\,\!}$${\displaystyle p?;a\,\!}$${\displaystyle a\,\!}$${\displaystyle \neg p?;b\,\!}$${\displaystyle a\cup 0\,\!}$${\displaystyle a\,\!}$${\displaystyle p\,\!}$${\displaystyle p\,\!}$

Конструкция while p do a реализуется как . Это выполняется ноль или более раз, а затем выполняется . Пока остается истинным, в конце блокирует исполнитель от преждевременного завершения итерации, но как только оно становится ложным, дальнейшие итерации тела блокируются, и исполнитель не имеет другого выбора, кроме как выйти через тест .${\displaystyle (p?;a)*;\neg p?\,\!}$${\displaystyle p?;a\,\!}$${\displaystyle \neg p?\,\!}$${\displaystyle p\,\!}$${\displaystyle \neg p?\,\!}$${\displaystyle p\,\!}$${\displaystyle \neg p?\,\!}$

Количественная оценка как случайное присвоение [ править ]

Оператор случайного присвоения обозначает недетерминированное действие установки произвольного значения. затем говорит, что сохраняется независимо от того, что вы устанавливаете , а говорит, что можно установить значение, которое делает истинным. таким образом, имеет то же значение, что и универсальный квантор , и аналогично соответствует экзистенциальному квантору . То есть логику первого порядка можно понимать как динамическую логику программ формы .${\displaystyle x:=?\,\!}$${\displaystyle x\,\!}$${\displaystyle [x:=?]p\,\!}$${\displaystyle p\,\!}$${\displaystyle x\,\!}$${\displaystyle \langle x:=?\rangle p\,\!}$${\displaystyle x\,\!}$${\displaystyle p\,\!}$${\displaystyle [x:=?]\,\!}$${\displaystyle \forall x\,\!}$${\displaystyle \langle x:=?\rangle \,\!}$${\displaystyle \exists x\,\!}$${\displaystyle x:=?\,\!}$

Дейкстра утверждал, что продемонстрировал невозможность программы, которая устанавливает значение переменной x в произвольное положительное целое число. ^[1] Однако в динамической логике с присваиванием и оператором *, x может быть установлено в произвольное положительное целое число с помощью программы динамической логики : следовательно, мы должны либо отклонить аргумент Дейкстры, либо признать, что оператор * неэффективен.${\displaystyle x:=0{\mathbin {;}}(x:=x+1){*}}$

Семантика возможного мира [ править ]

Модальная логика обычно интерпретируется с точки зрения возможного мира.семантика или структуры Крипке. Эта семантика естественным образом переносится в динамическую логику, интерпретируя миры как состояния компьютера в приложении для проверки программы или состояния нашей среды в приложениях к лингвистике, искусственному интеллекту и т. Д. Одна из ролей возможной семантики мира - формализовать интуитивные понятия истина и обоснованность, которые, в свою очередь, позволяют определить понятия разумности и полноты для систем аксиом. Правило вывода является правильным, когда действительность его посылок подразумевает обоснованность его вывода. Система аксиом является правильной, когда все ее аксиомы верны и правила вывода верны. Система аксиом считается полной, когда каждая действительная формула выводится как теорема этой системы. Эти концепции применимы ко всем системам логики, включая динамическую логику.

Пропозициональная динамическая логика (PDL) [ править ]

Обычная логика или логика первого порядка имеет два типа терминов, соответственно, утверждения и данные. Как видно из приведенных выше примеров, динамическая логика добавляет третий тип терминов, обозначающих действия. Динамическая логика утверждение содержит все три типа: , , и является данные, это действие, и и является утверждение. Логика высказываний выводится из логики первого порядка путем исключения терминов данных и аргументов только об абстрактных предложениях, которые могут быть простыми пропозициональными переменными или атомами, или составными предложениями, построенными с такими логическими связками, как и , или , и not .${\displaystyle [x:=x+1](x\geq 4)\,\!}$${\displaystyle x\,\!}$${\displaystyle x+1\,\!}$${\displaystyle 4\,\!}$${\displaystyle x:=x+1\,\!}$${\displaystyle x\geq 4\,\!}$${\displaystyle [x:=x+1](x\geq 4)\,\!}$

Пропозициональная динамическая логика, или PDL, была выведена из динамической логики в 1977 году Майклом Дж. Фишером и Ричардом Ладнером. PDL сочетает идеи, лежащие в основе логики высказываний и динамической логики, добавляя действия, опуская данные; следовательно, термины PDL - это действия и предложения. Приведенный выше пример TV выражен в PDL, тогда как следующий пример с участием - в DL первого порядка. PDL относится к динамической логике (первого порядка) так же, как логика высказываний относится к логике первого порядка.${\displaystyle x:=x+1\,\!}$

Фишер и Ладнер показали в своей статье 1977 года, что выполнимость PDL имела вычислительную сложность в большинстве случаев с недетерминированным экспоненциальным временем и, по крайней мере, с детерминированным экспоненциальным временем в худшем случае. Этот пробел был закрыт в 1978 году Воаном Праттом, который показал, что PDL разрешима за детерминированное экспоненциальное время. В 1977 году Кристер Сегерберг предложил полную аксиоматизацию PDL, а именно любую полную аксиоматизацию модальной логики K вместе с аксиомами A1-A6, как указано выше. Полнота доказательства для аксиом Segerberg были найдены Gabbay (неопубликованное примечание), Парикх (1978), Pratt (1979), и Кодзэн и Парикх (1981).

История [ править ]

Динамическая логика была разработана Воганом Праттом в 1974 году в заметках для класса по верификации программ как подход к приданию значения логике Хоара путем выражения формулы Хора как . Позже этот подход был опубликован в 1976 году как самостоятельная логическая система . Эта система параллельна системе алгоритмической логики Анджея Салвицкого ^[2] и концепции преобразователя предикатов с самым слабым предварительным условием Эдсжея Дейкстры , соответствующей системе Дейкстры.${\displaystyle p\{a\}q\,\!}$${\displaystyle p\to [a]q\,\!}$${\displaystyle \operatorname {wp} (a,p)\,\!}$${\displaystyle [a]p\,\!}$${\displaystyle \operatorname {wlp} (a,p)\,\!}$, самая слабая либеральная предпосылка. Однако эта логика не связана ни с модальной логикой, ни с семантикой Крипке, ни с регулярными выражениями, ни с исчислением бинарных отношений; поэтому динамическую логику можно рассматривать как уточнение алгоритмической логики и преобразователей предикатов, которое связывает их с аксиоматикой и семантикой Крипке модальной логики, а также с исчислениями бинарных отношений и регулярных выражений.

Проблема параллелизма [ править ]

Логика Хоара, алгоритмическая логика, слабейшие предварительные условия и динамическая логика - все они хорошо подходят для рассуждений и рассуждений о последовательном поведении. Однако распространение этой логики на параллельное поведение оказалось проблематичным. Существуют различные подходы, но всем им не хватает элегантности последовательного случая. Напротив, система темпоральной логики Амира Пнуэли 1977 г., другой вариант модальной логики, имеющий много общих черт с динамической логикой, отличается от всех вышеупомянутых логик тем, что Пнуэли охарактеризовал как «эндогенную» логику, а остальные - «экзогенные» логики. Под этим Пнуэли имел в виду, что утверждения временной логики интерпретируются в рамках универсальной поведенческой структуры, в которой одна глобальная ситуация изменяется с течением времени, тогда как утверждения других логик производятся извне по отношению к множеству действий, о которых они говорят. Преимущество эндогенного подхода состоит в том, что он не делает никаких фундаментальных предположений о том, что вызывает то, что окружающая среда изменяется со временем. Вместо этого временная логическая формула может говорить о двух несвязанных частях системы, которые, поскольку они не связаны между собой, неявно развиваются параллельно.По сути, обычное логическое соединение темпоральных утверждений является параллельным оператором композиции темпоральной логики. Простота этого подхода к параллелизму привела к тому, что темпоральная логика стала модальной логикой выбора для рассуждений о параллельных системах с ее аспектами синхронизации, интерференции, независимости, взаимоблокировки, динамической блокировки, справедливости и т. Д.

Эти проблемы параллелизма кажутся менее важными для лингвистики, философии и искусственного интеллекта, областей, в которых динамическая логика наиболее часто встречается в настоящее время.

Подробное описание динамической логики см. В книге Дэвида Харела и др. цитируется ниже.

См. Также [ править ]

Сноски [ править ]

Ссылки [ править ]

• Воан Пратт , "Семантические соображения по логике Флойда-Хора", Proc. 17-й ежегодный симпозиум IEEE по основам компьютерных наук, 1976, 109–121.
• Давид Харел , Декстер Козен и Ежи Тюрин , «Динамическая логика». MIT Press, 2000 (450 стр.).
• Дэвид Харел , «Динамическая логика», Д. Габбей и Ф. Гентнер, редакторы, Справочник по философской логике, том II: Расширения классической логики, глава 10, страницы 497-604. Рейдел, Дордрехт, 1984.
• Дэвид Харел , Декстер Козен и Ежи Тюрин , «Динамическая логика», Д. Габбай и Ф. Гентнер, редакторы, Справочник по философской логике, том 4: страницы 99–217. Kluwer, 2-е издание, 2002 г.

Внешние ссылки [ править ]

• Семантические соображения по логике Флойда-Хора (оригинальная статья по динамической логике)