Aritmética de Presburger

De Biquipédia
Saltar pa: nabegaçon, percura
Question book.svg
Este aneixo ó seçon nó cita nanhue fuonte ó refréncia, l que cumpromete sue credibelidade (zde dezembre de 2011).
Por fabor, melhore este artigo probidenciando fuontes fiables i andependientes, anserindo-las ne l cuorpo de l testo por meio de notas de rodapie. Ancontre fuontes: Googleamboras, libros, académicoScirusBing. Beija cumo referenciar i citar las fuontes.

Aritmética de Presburger ye la teorie de purmeira-orde de ls númaros naturales cun soma. Ten esse nome an honra de Mojżsç Presburger, l qual l'apersentou an 1929. L'assinatura de l'aritmética de Presburguer cuntén solo l'ouparaçon d'adiçon i eiqualizaçon, suprimindo l'ouparaçon de multiplicaçon totalmente. Esso anclui l squema d'anduçon.

Aritmética de Presburger ye mui mais fraca de l que Peano aritmética, qu'anclui tanto l'ouparaçon d'adiçon quanto la de multiplicaçon. Al cuntrairo de l'aritmética de Peano, l'aritmética de Presburger ye ua teorie decidible. Esto senefica que ye possible efetibamente detreminar, por qualquiera sentença na lenguaige de l'aritmética Presburger, se essa frase ye dedutible de ls axiomas de l'aritmética de Presburger. L tiempo de funcionamiento assintótico cumplexidade cumputacional deste porblema de decison ye duplamente sponencial, cumo mostrado por Fischer i Rabin (1974).

Bison global[eiditar | editar código-fonte]

La lenguaige de l'aritmética de Presburger cuntén custantes 0 i 1 i la funçon binária +, anterpretada cumo adiçon. Nessa léngua, ls axiomas de l'aritmética Presburger son l'ounibersal fechamiento de ls 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) fur ua fórmula de purmeira orde na lenguaige de l'aritmética de Presburger cun ua bariable libre X (i possiblemente outras bariables ​​libres), anton la fórmula segue un axioma:

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

(5) ye un squema d'axioma de l'anduçon, l que repersenta un númaro anfenito d'axiomas. Ua beç que ls axiomas ne l squema an (5) nun puoden ser sustituídos por qualquiera númaro fenito d'axiomas, l'aritmética de Presburger nun ye fenitamente axiomatizable. L'aritmética de Presburger nun puode formalizar cunceitos tales cumo la debesibelidade ó l númaro primo. Giralmente, qualquiera cunceito de númaro liebando la multiplicaçon nun puode ser defenida na aritmética de Presburger, ua beç que lieba a l'ancumpletude i andecidibelidade. Inda assi, puode-se formular eisemplos andebiduales de debesibelidade, cumo, por eisemplo, se rebelar "para to x, eisiste y: (y + y = x) ∨ (y + y + 1 = x)". Esto andica que cada númaro ye par ó ímpar.

Propiadades[eiditar | editar código-fonte]

Mojżsç Presburger probou que l'aritmética de Presburger ye:

  • cunsistente: Nun hai nanhue declaraçon na aritmética de Presburger que puode ser deduzida a partir de ls axiomas de tal forma que sue negaçon puode tamien ser deduzida.
  • cumpleto: Para cada anstruçon na aritmética de Presburger, ó ye possible deduzi-l'a partir de ls axiomas ó ye possible deduzir la sue negaçon.
  • decidible: Eesiste un algoritmo, que decide se qualquiera declaraçon dada na aritmética de Presburger ye berdadeira ó falsa.

La decidibelidade na aritmética de Presburger puode ser repersentada outelizando eliminaçon de quantificadores, cumplementados por raciocinar subre cungruéncia aritmética (Anderton 2001, p. 188).

Peano aritmética, que ye l'aritmética de Presburger oumentada cula multiplicaçon, nun ye detreminable, cumo ua cunsequéncia de la repuosta negatiba al Entscheidungsproblen. Pul teorema de l'ancumpletude de Gödel, l'aritmética de Peano ye ancumpleta i sue cunsisténcia nun ye demunstrable anternamente.

L porblema de decison pa l'aritmética de Presburger ye un eisemplo antressante an teorie de la cumplexidade cumputacional i cumputaçon. Seia m l cumprimiento dua anstruçon an aritmética de Presburger. An seguida, Fischer i Rabin (1974) probórun que qualquiera algoritmo de decison pa l'aritmética de Presburger ten un tiempo d'eisecuçon ne l pior causo de pul menos  2 ^ {2 ^ {cn}} , para algua custante c> 0. Assi, l porblema de decison para aritmética de Presburger ye un eisemplo dun porblema de decison que ten sido demunstrada para eisigir mais de l que l tiempo d'eisecuçon sponencial. Fischer i Rabin tamien probórun que para qualquiera axiomatizaçon razoable (defenida percisamente an sou artigo), eisisten teoremas de cumprimiento m que ténen duplamente sponencial probas de cumprimiento. Antuitibamente, esto senefica qu'eisisten lemites cumputacionales subre l que puode ser cumprobado por porgramas de cumputador. L trabalho de Fischer i Rabin tamien amplica que l'aritmética de Presburger puode ser outelizada para defenir fórmulas que calculan corretamente qualquiera algoritmo, zde que las antradas stéian drento de lemites relatibamente grandes. Ls lemites puoden ser oumentados, mas solo usando nuobas fórmulas. Por outro lado, un lemite superior dua sponencial tripla para un procedimiento de decison pa l'aritmética de Presburger fui probado por Ouppen (1978).

Aplicaçones[eiditar | editar código-fonte]

Cumo ye probable la decidibelidade de l'aritmética de Presburger, proba outomática de teoremas algoritmos de berificaçon de teoremas la cunsidran bálida na aritmética. (Por eisemplo, l sistema assistente de proba Coq apersenta ua tática para aritmética de Presburger.) La cumplexidade sponencial dupla de la teorie torna ampraticable ousar ls probadores de teorema subre fórmulas cumplicadas, mas este cumportamiento ocorre solo na persença de quantificadores amarrados: Ouppen i Nelson (1980) çcriben un probador de teoremas outomático qu'usa l algoritmo simplex nua aritmética de Presburger stendida sin quantificadores amarrados. L'algoritmo simplex ten tiempo de pior causo sponencial an eisecuçon, mas eisibe eficiéncia cunsidrabelmente melhor para anstáncias típicas de la bida rial. Tiempo d'eisecuçon sponencial ye ouserbado solo pa ls causos specialmente custruídos. Esto faç cun qu'ua abordaige baseada an simplex seia prática nun sistema de trabalho.

Refréncias[eiditar | editar código-fonte]

Ligaçones sternas[eiditar | editar código-fonte]

  • online prober La Jaba applet probes or çprobes arbitrary formulas of Presburger arithmetic (In German)
  • [1] La cumplete Theoren Prober fur Presburger Arithmetic by Phelipp Rummer
Wiki letter w.svg Este artigo ye un rabisco. Tu puodes ajudar la Biquipédia acrecentando-lo.