Aritmética de Presburger

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Question book.svg
Esta página ou secção não cita nenhuma fonte ou referência, o que compromete sua credibilidade (desde dezembro de 2011).
Por favor, melhore este artigo providenciando fontes fiáveis e independentes, inserindo-as no corpo do texto por meio de notas de rodapé. Encontre fontes: Googlenotícias, livros, acadêmicoYahoo!Bing. Veja como referenciar e citar as fontes.

Aritmética de Presburger é a teoria de primeira-ordem dos números naturais com soma. Tem esse nome em honra de Mojżesz Presburger, o qual a apresentou em 1929. A assinatura da aritmética de Presburguer contém apenas a operação de adição e equalização, suprimindo a operação de multiplicação totalmente. Isso inclui o esquema de indução.

Aritmética de Presburger é muito mais fraca do que Peano aritmética, que inclui tanto a operação de adição quanto a de multiplicação. Ao contrário da aritmética de Peano, a aritmética de Presburger é uma teoria decidível. Isto significa que é possível efetivamente determinar, por qualquer sentença na linguagem da aritmética Presburger, se essa frase é dedutível dos axiomas da aritmética de Presburger. O tempo de funcionamento assintótico complexidade computacional deste problema de decisão é duplamente exponencial, como mostrado por Fischer e Rabin (1974).

Visão global[editar | editar código-fonte]

A linguagem da aritmética de Presburger contém constantes 0 e 1 e a função binária +, interpretada como adição. Nessa língua, os axiomas da aritmética Presburger são o universal fechamento dos seguintes:

  1. ¬(0 = x + 1)
  2. x + 1 = y + 1 → x = y
  3. x + 0 = x
  4. (x + y) + 1 = x + (y + 1)

Se P (x) for uma fórmula de primeira ordem na linguagem da aritmética de Presburger com uma variável livre X (e possivelmente outras variáveis ​​livres), então a fórmula segue um axioma:

(P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y)

(5) é um esquema de axioma da indução, o que representa um número infinito de axiomas. Uma vez que os axiomas no esquema em (5) não podem ser substituídos por qualquer número finito de axiomas, a aritmética de Presburger não é finitamente axiomatizable. A aritmética de Presburger não pode formalizar conceitos tais como a divisibilidade ou o número primo. Geralmente, qualquer conceito de número levando a multiplicação não pode ser definida na aritmética de Presburger, uma vez que leva à incompletude e indecidibilidade. No entanto, pode-se formular exemplos individuais de divisibilidade, como, por exemplo, se revelar "para todo x, existe y: (y + y = x) ∨ (y + y + 1 = x)". Isto indica que cada número é par ou ímpar.

Propriedades[editar | editar código-fonte]

Mojżesz Presburger provou que a aritmética de Presburger é:

  • consistente: Não há nenhuma declaração na aritmética de Presburger que pode ser deduzida a partir dos axiomas de tal forma que sua negação pode também ser deduzida.
  • completo: Para cada instrução na aritmética de Presburger, ou é possível deduzi-la a partir dos axiomas ou é possível deduzir a sua negação.
  • decidível: Existe um algoritmo, que decide se qualquer declaração dada na aritmética de Presburger é verdadeira ou falsa.

A decidibilidade na aritmética de Presburger pode ser representada utilizando eliminação de quantificadores, complementados por raciocinar sobre congruência aritmética (Enderton 2001, p. 188).

Peano aritmética, que é a aritmética de Presburger aumentada com a multiplicação, não é determinável, como uma consequência da resposta negativa ao Entscheidungsproblem. Pelo teorema da incompletude de Gödel, a aritmética de Peano é incompleta e sua consistência não é demonstrável internamente.

O problema de decisão para a aritmética de Presburger é um exemplo interessante em teoria da complexidade computacional e computação. Seja n o comprimento de uma instrução em aritmética de Presburger. Em seguida, Fischer e Rabin (1974) provaram que qualquer algoritmo de decisão para a aritmética de Presburger tem um tempo de execução no pior caso de pelo menos  2 ^ {2 ^ {cn}} , para alguma constante c> 0. Assim, o problema de decisão para aritmética de Presburger é um exemplo de um problema de decisão que tem sido demonstrada para exigir mais do que o tempo de execução exponencial. Fischer e Rabin também provaram que para qualquer axiomatização razoável (definida precisamente em seu artigo), existem teoremas de comprimento n que têm duplamente exponencial provas de comprimento. Intuitivamente, isto significa que existem limites computacionais sobre o que pode ser comprovado por programas de computador. O trabalho de Fischer e Rabin também implica que a aritmética de Presburger pode ser utilizada para definir fórmulas que calculam corretamente qualquer algoritmo, desde que as entradas estejam dentro de limites relativamente grandes. Os limites podem ser aumentados, mas apenas usando novas fórmulas. Por outro lado, um limite superior de uma exponencial tripla para um procedimento de decisão para a aritmética de Presburger foi provado por Oppen (1978).

Aplicações[editar | editar código-fonte]

Como é provável a decidibilidade da aritmética de Presburger, prova automática de teoremas algoritmos de verificação de teoremas a consideram válida na aritmética. (Por exemplo, o sistema assistente de prova Coq apresenta uma tática para aritmética de Presburger.) A complexidade exponencial dupla da teoria torna impraticável usar os provadores de teorema sobre fórmulas complicadas, mas este comportamento ocorre apenas na presença de quantificadores aninhados: Oppen e Nelson (1980) descrevem um provador de teoremas automático que usa o algoritmo simplex em uma aritmética de Presburger estendida sem quantificadores aninhados. O algoritmo simplex tem tempo de pior caso exponencial em execução, mas exibe eficiência consideravelmente melhor para instâncias típicas da vida real. Tempo de execução exponencial é observado apenas para os casos especialmente construídos. Isto faz com que uma abordagem baseada em simplex seja prática em um sistema de trabalho.

Referências[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]

  • online prover A Java applet proves or disproves arbitrary formulas of Presburger arithmetic (In German)
  • [1] A complete Theorem Prover for Presburger Arithmetic by Philipp Rümmer
Wiki letter w.svg Este artigo é um esboço. Você pode ajudar a Wikipédia expandindo-o. Editor: considere marcar com um esboço mais específico.