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 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 ().
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 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 ).
A1.
A2.
A3.
A4.
A5.
A6.
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 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
"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.
Regras derivadas de inferência 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.
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.
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.
Atribuição 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.
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.
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.
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.
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.
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 .
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.
Teste 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.
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.