Lógica dinâmica
 |
Lógica dinâmica é uma extensão da lógica modal originalmente planejada para raciocinar sobre programas de computador e, posteriormente, aplicada a mais comportamentos complexos gerais decorrentes da linguística, filosofia, Inteligência Artificial, e outros campos.
Linguagens
[editar | editar código-fonte]Logica modal é caracterizada pelos operadores modais (box p) afirmando que é necessariamente o caso, e (diamond p) afirmando que p\,\! é possivelmente o caso. Lógica dinâmica estende isso associando a cada ação os operadores modais e , assim formando a lógica multimodal. O significado de é que depois de executar uma ação é necessariamente o caso que se verifica, isto é, deve acarretar . O significado de é que depois de realizar é possivel que se verifique, ou seja, deve acarretar . Estes operadores estão relacionados por e , analogamente para a relação entre quantificadores universais () e existenciais ().
![{\displaystyle [a]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a1fb5b3d73ccbb07fc5a491131c0322f70356187)
![{\displaystyle [a]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/62ca72b8b7c76d167780fd376152ae5edd1aa688)
![{\displaystyle [a]p\equiv \neg \langle a\rangle \neg p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7bde1dc564fab0e836c086f63503aefe507a211e)
![{\displaystyle \langle a\rangle p\equiv \neg [a]\neg p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6d4befef130a766d84e4c1aa6f468f53cc4393bb)
Lógica dinâmica permite ações compostas construídas a partir de ações menores. Enquanto os operadores de controle de base de qualquer linguagem de programação pode ser utilizada para este fim, operadores de expressão regular de Kleene são uma boa combinação para a lógica modal. Dadas ações e , a componente , escolha, pode-se escrever também ou , é realizada através da realização de um dos ou . O componente , sequencia, é realizado efetuando primeiro e depois . O componente , iteração, é é realizado efetuando zero ou mais vezes, sequencialmente. A constante ou BLOCK não faz nada e não finaliza, ao passo que a constante ou SKIP ou NOP, definivel como , não faz nada porém finaliza.
Axiomas
[editar | editar código-fonte]Esses operadores podem ser axiomatizada pela lógica dinâmica da seguinte forma, tomando como já dado uma axiomatização adequada de lógica modal incluindo os axiomas para operadores modais como o axioma acima mencionad e as duas regras de inferência modus ponens ( e implica) e necessitarão ( implica ).
![{\displaystyle \vdash [a]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/32ac01f45918dddcfa2a3102efb608a21d9549c4)
A1.
![{\displaystyle [0]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2243a8da2a7d9c6ac5fd5a27d57a1638e440a72f)
A2.
![{\displaystyle [1]p\equiv p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/556a749d59c561b718d377fe2621c98858939512)
A3.
![{\displaystyle [a\cup b]p\equiv [a]p\land [b]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97e8b5f15edf169b04e0e25ee20821f35f9db959)
A4.
![{\displaystyle [a;b]p\equiv [a][b]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/65ad236140af11ab74ca4b183ed49dce7034195a)
A5.
![{\displaystyle [a*]p\equiv p\land [a][a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/241342dedcc18e38632d8b393feced26f1728019)
A6.
\to [a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/596a5affc1e9f43a0389e75c7aea2479d05fd014)
Axiom A1 faz a promessa vazia que quando o BLOCK termina, vai manter, mesmo que é a proposição 'falsa. (Assim, 'BLOCK abstrai a essência da ação do inferno congelar de novo.)
A2 diz que [NOP] age como a função identidade em proposições, ou seja, ele transforma em si mesmo.
A3 diz que se fazer um dos ou deve acarretar , então deve acarretar e também para , e vice-versa.
A4 diz que se fazer e deve acarretar , then deve acarretar a uma situação em que deve acarretar .
A5 é o resultado evidente de aplicação de , A3 e A4 à equação de de "Kleene álgebra".
A6 afirma que, se se verifica agora , e não importa quantas vezes fazemos continua a ser a veracidade de depois que a execução implica a sua veracidade, depois de mais uma execução de , então deve permanecer verdadeiro não importa quantas vezes fazemos . A6 é reconhecível como indução matemática com a ação n := n+1 de incrementar n generalizada de ações arbitrárias . <br
Derivações
[editar | editar código-fonte]O axioma da lógica modal permite a obtenção das seguintes seis teoremas correspondentes a seguir:
T1.
T2.
T3.
T4.
T5.
T6.
T1 afirma a impossibilidade de acarretar qualquer coisa ao realizar BLOCK.
T2 observa novamente que NOPmuda nada, tendo em conta que NOP é tanto determinista e finalizador donde e tem a mesma força.
T3 diz que, se a escolha do um ou poderia acarretar em p , Em seguida, tanto quanto sozinhos poderia acarretar .
T4 é como A4.
T5 é explicada como a A5.
T6 se afirma que é possível conseguir efetuando suficientemente, em seguida é verdade agora ou é possível executar repetidamente para criar uma situação em que (ainda) é falsa, mas mais uma execução de poderia acarretar .<br
![{\displaystyle [1]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/76fdef3b81c82f740f94bda91755a8ee95bea6f1)
"Box" e "diamante" são totalmente simétricos em relação ao qual se toma como primitivo. Uma axiomatização alternativa teria sido a tomar o teoremas T1-T6 como axiomas, a partir do qual poderíamos, então, ter derivados A1-A6 como teoremas.
A diferença entre implicação e inferência é a mesma em lógica dinâmica como em qualquer outra lógica: enquanto a implicação afirma que, se é verdade, então que assim seja , a inferência afirma que, se é válida, então que assim seja . No entanto, a natureza dinâmica da lógica dinâmica move esta distinção fora do reino de axiomática abstratas para a experiência de senso comum de situações em fluxo. A regra de inferência , for example, por exemplo, é o som, pois sua premissa afirma que detém em todos os momentos, de onde, não importa onde um pode nos levar, será verdade. A implicação não é válido, porque a verdade de no momento atual não é garantida a sua veracidade após a realização de . Por exemplo, será verdade em qualquer situação onde é falso, ou em qualquer situação onde é verdade, mas a afirmação é falsa em qualquer situação onde tem o valor 1, e, portanto, não é válida.
![{\displaystyle p\vdash [a]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1e3d4111e86ea26cccf17376fb9595d1ac982313)
![{\displaystyle p\to [a]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/25333da70b990f4a843fafa918b10a0287fbcbd5)
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f06f0d0b572bdd220c15a0f12238a08496299518)
Regras derivadas de inferência
[editar | editar código-fonte]Quanto à lógica modal, as regras de inferência modus ponens' e necessitação também bastam para a lógica dinâmica como as únicas regras primitivas de que necessita, como descrito acima. No entanto, como é habitual na lógica, muito mais regras podem ser derivadas a partir destas, com a ajuda dos axiomas. Um exemplo de instância de uma regra derivada em lógica dinâmica é que, se chutar uma TV quebrada uma vez não há como consertá-la, em seguida, repetidamente chutá-la não pode consertá-la também. Escrita para a ação de chutar a TV, e para a proposição de que a TV está quebrada, a lógica dinâmica expressa esta inferência como , tendo como premissa e, como conclusão .O significado de é que é garantido que depois de chutar a TV, ela está quebrada. Daí a premissa significa que se a TV está quebrada, então depois de chutá-la, uma vez que ainda vai continuar quebrada. denota a ação de chutar a TV zero ou mais vezes. Daí a conclusão significa que se a TV está quebrado, então depois chutando zero ou mais vezes ainda vai continuar quebrada. Porque, se não, depois do segundo ao último chute a TV estaria em um estado onde chutando-a uma vez mais iria consertá-lo, que as reivindicações premissa nunca pode acontecer em qualquer circunstância.
![{\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/62d0f1dce56bcad6e2fed130d59b49aec18e728a)
![{\displaystyle b\to [k]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a80357a9742d2223221e74a92ae1f4e1e8ba445e)
![{\displaystyle b\to [k*]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e656caffdc43024ca5be23536741ff4946214517)
![{\displaystyle [k]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d4f9fa4da5dcef257a7a39cb7fc502044c1993d8)
A inferência é o som. No entanto, a implicação não é válida porque podemos facilmente encontrar situações em que se mantem mas não. Em qualquer situação contra-exemplo, deve manter, mas deve ser falso, enquanto deve ser verdade. Mas isso pode acontecer em qualquer situação em que a TV está quebrada, mas pode ser revivido com dois chutes. A implicação falhar (não é válido), porque ele só exige que segure agora, enquanto a inferência sucede (é som), porque ele requer que manter em todas as situações, e não apenas a atual.
![{\displaystyle (b\to [k]b)\to (b\to [k*]b)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c1e1a37706b4e0882227d6b43de44df679cb1aef)
![{\displaystyle [k*]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4f183003713ca95bab7f66b8a8e0d9f39df156ee)
Um exemplo de uma implicação válida é a proposição . Este diz que se é maior ou igual a 3, depois de incrementação de , deve ser maior ou igual a 4. No caso de ações deterministas que está garantido para terminar, como , "pode" e "deve" ter a mesma força, ou seja, and tem o mesmo significado. Daí a proposta anterior, é equivalente a afirmando que se é maior ou igual a 3, em seguida, após realização , pode ser maior ou igual a 4.
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bc161d9b9d88878ef16af585a731fb107f67f63b)
Atribuição
[editar | editar código-fonte]A forma geral de um comando de atribuição é onde é uma variável e é uma expressão construída a partir de constantes e variáveis com o que quer que as operações são fornecidos pela linguagem, como adição e multiplicação. O axioma Hoare para a atribuição não é dado como um único axioma, mas sim como um esquema de axioma.
A7.
![{\displaystyle [x:=e]\Phi (x)\equiv \Phi (e)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/afe13e96391214b1dbd3af87dd5757c288e8af77)
Este é um esquema no sentido de que pode ser instanciado com qualquer fórmula containing contendo zero ou mais ocorrências de uma variável . O significado de é com essas ocorrências que ocorre livre em ,Ou seja, não vinculados por algum quantificador como em , Substituído por . Por exemplo, podemos instanciar A7 com , Ou com . Tal esquema axiomatico permite um número infinito de axiomas ter um formulário comum a escrita como uma expressão finita conotando essa forma.
\equiv e=y^{2}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3d32bd8cfd0d26ae5f4ec067262f83498f757660)
\equiv b=c+e\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7d174a2b325ec065684d7ad628416e1f5e69262f)
A instância da A7 nos permite calcular mecanicamente que o exemplo encontrado alguns parágrafos atrás é equivalente a , Que por sua vez é equivalente a pela álgebra elementar.
\equiv (x+1)\geq 4\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/be8e2a29c817d594b130ef17fe24181f7bbdb560)
![{\displaystyle [x:=x+1]x\geq 4\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7f65816abeab4b4d94fe1d648e60f32d76fb9d47)
Um exemplo que ilustra a atribuição, em combinação com é a proposição . Este afirma que é possível, incrementando suficientemente, muitas vezes, para fazer igua a 7. Isto, obviamente, nem sempre é verdade, por exemplo, se é de 8 para começar, ou 6.5, de onde esta proposição não é um teorema da lógica dinâmica. Se é do tipo inteiro no entanto, esta proposição é verdadeira se e somente se é, no máximo, 7, para começar, ou seja, ela é apenas uma maneira indireta de dizer .
Indução matemática pode ser obtido como o exemplo de A6, em que a proposição é instanciado como , a ação como , e como . As duas primeiras dessas três instâncias são simples, convertendo a A6 . No entanto, a simples substituição de ostensivamente para não é tão simples, pois traz à tona o chamado opacidade referencial da lógica modal, no caso quando uma modalidade pode interferir com uma substituição.
\to [n:=n+1]\Phi (n)))\to [(n:=n+1)*]\Phi (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/387b4dd2f085e5a8f4a98bcd89bca88811a94cf8)
Quando substituído para , estávamos pensando no símbolo proposição como um designador rígido com respeito à modalidade , que significa que é a mesma proposição após incrementando como antes, embora incrementando podem afetar sua verdade. Do mesmo modo, a ação ainda é a mesma ação depois incrementando , embora incrementando resultará em sua execução em um ambiente diferente. No entanto, em si não é um designador rígido com respeito à modalidade ; e, se ele denota 3 antes incrementando , denota 4 depois. Portanto, não podemos apenas substituir para em todos os lugares em A6.
![{\displaystyle [n:=n+1]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/044fb0d8c92e5e7228efb8f16bf07edf10216353)
Uma forma de lidar com a opacidade das modalidades é eliminá-los. Para este fim, expandir como o conjunto infinito , Isto é, o conjunto durante toda de . Agora aplique A4 para transformar em , possuindo modalidades. Em seguida, aplique o axioma de Hoare vezes a este para produzir , então simplificar este conjunto infinito de . Esta redução todo deve ser aplicado a ambas as instâncias do na A6, originando . A modalidade remanescente pode agora ser eliminados com mais um uso do axioma de Hoare para dar .
![{\displaystyle [(n:=n+1)*]\Phi (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/87f13127d75cee89f7e659c3807d4fe801583058)
![{\displaystyle [(n:=n+1)^{0}]\Phi (n)\land [(n:=n+1)^{1}]\Phi (n)\land [(n:=n+1)^{2}]\Phi (n)\land \ldots \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/04e959dd47b2fdde55833b0755833bd0deefe611)
![{\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/59da810a92ad42e14b5c4b17a69aa35c93e2cca2)
![{\displaystyle [n:=n+1][n:=n+1]\ldots \Phi (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7caacf5aab8e5b04d1f275a84143f124cde2132f)
![{\displaystyle [(n:=n+1)*]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b3e0a9d62923411630e49bdac5651338095541a7)
![{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to [n:=n+1]\Phi (n+i)))\to \forall i\Phi (n+i)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/64af1426c5434142818e7aea3a0fa53e25aec648)
Com as modalidades opacos agora fora do caminho, podemos substituir com segurança para na forma usual de lógica de primeira ordem para obter Peano é celebrado axioma , indução ou seja matemático.
Uma sutileza que encoberto aqui é que deve ser entendido como que varia ao longo dos números naturais, em que é o expoente na expansão de como a união de sobre todos os números naturais . A importância de manter esta informação digitação se torna reta aparente se tinha sido do tipo inteiro, ou mesmo real, para qualquer um dos que A6 é perfeitamente válido como um axioma. Como um exemplo disso, se é uma variável real e é o predicado é um número natural, então axioma A6 após as duas primeiras substituições, ou seja, , é igualmente válida, isto é, a verdadeira em cada estado, independentemente do valor de nesse estado, como quando é do tipo número natural. Se em um determinado estado é um número natural, então o antecedente do principal implicação A6 detém, mas, em seguida, também é um número natural, para a conseqüente também detém. Se não é um número natural, então o antecedente é falso e assim A6 permanece verdadeiro, independentemente da verdade do conseqüente. Podemos fortalecer A6 para uma equivalência sem afetar nada disso, o outro sentido de ser provada a partir de A5, a partir do qual podemos ver que, se o antecedente de A6 acontece ser falsa em algum lugar, em seguida, o conseqüente deve ser falsa.
\equiv [a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b06d3a2faff030e5d62b60f4b9be85bb59aae85a)
Teste
[editar | editar código-fonte]Associados lógica dinâmica para cada proposição uma ação chamado um ensaio. Quando detém, o teste atua como um NOP, mudando nada, permitindo a ação de seguir em frente. Quando é falso, atua como BLOCK. Os testes podem ser axiomatizada como se segue.
A8.
![{\displaystyle [p?]q\equiv p\to q\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/085742eaef61fb7932fa3205bbb2fe38a9b168a9)
O teorema correspondente para é:
T8.
A construção se p então uma outra b é realizado em lógica dinâmica como . Esta ação expressa uma escolha guardado: se detém, em seguida, é equivalente a , enquanto é equivalente ao "bloco" e é equivalente a . Assim, quando é verdade que o performer da ação só pode tomar o ramo esquerdo, e quando é falsa a direita.
A construção, enquanto que p faz a realizado como . Isso realiza zero ou mais vezes e em seguida, executa . Enquanto que ontinua a ser verdade, a nos blocos finais do performer de terminar a iteração prematuramente, mas assim que ela se torna falso, mais iterações do corpo são bloqueados e, em seguida, o cantor não tem escolha, mas para sair através do teste .
Quantificação como atribuição aleatória
[editar | editar código-fonte]A declaração de atribuição aleatória denota a ação não determinístico de criação para um valor arbitrário. em seguida, diz que detém, não importa o que você definir a, enquanto diz que é possível definir para um valor que faz verdade. assim, tem o mesmo significado que o quantificador universal , enquanto similarmente corresponde ao quantificador existencial . Ou seja, a lógica de primeira ordem pode ser entendida como a lógica de programas de dinâmica a forma .
![{\displaystyle [x:=?]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f64442623ad98fcf93d35bfaa4773e4a786391ff)
![{\displaystyle [x:=?]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f7a670b697124c9df80b3f95675e9e69863f0d30)
Semântica de mundos possíveis
[editar | editar código-fonte]Lógica modal é mais comumente interpretada em termos de possíveis mundo semântica ou estruturas de Kripke. Esta semântica transporta mais naturalmente a lógica dinâmica interpretando mundos como estados de um computador na aplicação de programa de verificação, ou estados de nosso ambiente de aplicações para a linguística, AI, etc. Um papel para possíveis semântica de mundos é formalizar as noções intuitivas de verdade e validade, que por sua vez permitem que as noções de solidez e integridade a ser definida para sistemas axiomáticos. Uma regra de inferência é emitido quando a validade de suas premissas implica na validade da sua conclusão. Um sistema de axioma é boa quando todos os seus axiomas são válidas e as suas regras de inferência são sólidos. Um sistema de axioma é completa quando cada fórmula válida é derivável como um teorema desse sistema. Esses conceitos se aplicam a todos os sistemas de lógica , incluindo a lógica dinâmica.
Lógica dinâmica proposicional
[editar | editar código-fonte]Ordinário ou lógica de primeira ordem tem dois tipos de termos, respectivamente afirmações e dados. Como pode ser visto a partir dos exemplos acima, a lógica dinâmica adiciona um terceiro tipo de acções de duração denotando. A afirmação lógica dinâmica contém todos os três tipos: , , e são dados, é uma ação, e e são afirmações. lógica proposicional é derivado da lógica de primeira ordem, omitindo termos de dados e razões apenas cerca de proposições abstratas, que podem ser simples variáveis proposicionais ou átomos ou proposições compostas construídas com esses conectivos lógicos como AND, OR e NOT.
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c7fcfa23d464f4776e68d47af0f174364ea6173)
Lógica dinâmica proposicional, ou PDL, foi derivado de lógica dinâmica em 1977 por Michael J. Fischer e Richard Ladner. PDL combina as ideias por trás lógica proposicional e lógica dinâmica, adicionando ações, enquanto a omissão de dados, daí os termos do PDL são ações e proposições. O exemplo da TV acima é expressa em PDL considerando que o próximo exemplo envolvendo está na primeira ordem DL. PDL é (de primeira ordem) lógica dinâmica como a lógica proposicional é a lógica de primeira ordem.
Fischer e Ladner mostraram em seu artigo de 1977 que satisfatibilidade em PDL é de complexidade computacional, no máximo, tempo exponencial não determinístico, e pelo menos tempo exponencial determinístico no pior caso. Esta lacuna foi fechada em 1978 por Vaughan Pratt, que mostrou que PDL era decidível em tempo exponencial determinístico. Em 1977, Krister Segerberg propôs uma axiomatização completa do PDL, ou seja, qualquer axiomatização completa de lógica modal K juntamente com axiomas A1-A6 como dado acima. Provas de completude dos axiomas de Segerberg foram encontradas por Gabbay (nota não publicada), Parikh (1978), Pratt (1979), e Kozen e Parikh (1981).
História
[editar | editar código-fonte]Lógica Dinâmica foi desenvolvida por Vaughan Pratt em 1974 em notas para uma disciplina sobre verificação de programas como uma abordagem para a atribuição de sentido à lógica de Hoare, expressando a fórmula de Hoare as . A abordagem foi posteriormente publicado em 1976 como um sistema lógico em si próprio. Os sistemas paralelos "sistema de algoritimo lógico de A. Salwicki" e "noção de transformadores de predicado de pré-condição mais fraca de Edsger Dijkstra" . Com correspondendo à pré-condição liberal mais fraca de Dijkstra . Essas lógicas no entanto não estabeleceram nenhuma ligação com lógica modal, a semântica de Kripke, expressões regulares, ou o cálculo de relações binárias; lógica dinâmica, portanto, pode ser vista como um refinamento da lógica algorítmica e transformadores de predicados que a conecta com a axiomática e a semântica de Kripke da modal lógica, bem como para o cálculo de relações binárias e expressões regulares.
![{\displaystyle p\to [a]q\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8e1788859ff60725bc56a43ac4d5ecc072ea6b4)
o "Concurrency Challenge"
[editar | editar código-fonte]A lógica de Hoare, a lógica algorítmica, as pré-condições mais fracas, e a lógica dinâmica são todas bem adaptadas ao discurso e raciocínio sobre o comportamento sequencial. Estender essas lógicas para comportamento concorrente no entanto revelou-se problemático. Existem várias abordagens, mas todas elas carecem da elegância do caso seqüencial. Por outro lado, o sistema de lógica temporal de Amir Pnueli de 1977, outra variante da lógica modal que compartilha muitas características em comum com a lógica dinâmica, é diferente de todas as lógicas acima mencionadas por ser o que Pnueli caracterizou como uma lógica "endógena", sendo as outras lógicas "exógenas". Por isso Pnueli quis dizer que as afirmações lógicas temporais são interpretadas dentro de um quadro comportamental universal em que uma única situação global muda com o passar do tempo, ao passo que as afirmações das outras lógicas são feitas externamente às várias ações sobre as quais elas falam. A vantagem da abordagem endógena é que ela não faz suposições fundamentais sobre o que causa o que como o ambiente muda com o tempo. Ao contrário, uma fórmula lógica temporal pode falar de duas partes independentes de um sistema, que, porque eles não estão relacionados tacitamente evoluir em paralelo. Com efeito conjunção lógica comum de afirmações temporais é o operador de composição simultânea de lógica temporal. A simplicidade desta abordagem para a concorrência resultou em lógica temporal sendo a lógica modal de escolha para o raciocínio sobre sistemas concorrentes com seus aspectos de sincronização, interferência, independência, impasse, justiça, etc. Essas preocupações de concorrência parece ser menos críticas para a linguística, filosofia e inteligência artificial, as áreas em que a lógica dinâmica é mais frequentemente encontrada hoje em dia.
Referências
[editar | editar código-fonte]- Vaughan Pratt, "Semantical Considerations on Floyd-Hoare Logic", Proc. 17th Annual IEEE Symposium on Foundations of Computer Science, 1976, 109-121.
- David Harel, Dexter Kozen, and Jerzy Tiuryn, "Dynamic Logic". MIT Press, 2000 (450 pp).
- David Harel, "Dynamic Logic", In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, chapter 10, pages 497-604. Reidel, Dordrecht, 1984.
Ligações externas
[editar | editar código-fonte]- Semantical Considerations on Floyd-Hoare Logic(original paper on dynamic logic)
