Aritmética de Presburger

A Aritmética de Presburger é uma 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.

A Aritmética de Presburger é muito mais fraca do que a aritmética de Peano, 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

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

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).

A aritmética de Peano, 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

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

• Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence. Edinburgh University Press: 91–100.
• Enderton, Herbert (2001). A mathematical introduction to logic 2ª ed. Boston, MA: Academic Press. ISBN 978-0-12-238452-3 
• Ferrante, Jeanne, and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718. Springer-Verlag.
• Fischer, M. J., and Michael O. Rabin, 1974, ""Super-Exponential Complexity of Presburger Arithmetic." Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7: 27–41.
• G. Nelson and D. C. Oppen (abril de 1978). «A simplifier based on efficient decision algorithms». Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 141–150. doi:10.1145/512760.512775 
• Mojżesz Presburger, 1929, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt" in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101.
• William Pugh, 1991, "The Omega test: a fast and practical integer programming algorithm for dependence analysis,".
• Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation." ACM Symposium on Theory of Computing: 320–325.
• Young, P., 1985, "Godel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition" in A. Nerode and R. Shore, Recursion Theory, American Mathematical Society: 503-522.
• Derek C. Oppen: A 2^22pn Upper Bound on the Complexity of Presburger Arithmetic. J. Comput. Syst. Sci. 16(3): 323-332 (1978) doi:10.1016/0022-0000(78)90021-1

Ligações externas

• 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