WikiSort.ru - Не сортированное

ПОИСК ПО САЙТУ | о проекте

Арифметика Пресбургера — это теория первого порядка, описывающая натуральные числа со сложением, но в отличие от арифметики Пеано, исключающая высказывания относительно умножения. Названа в честь польского математика Мойжеша Пресбургера, который в 1929 году предложил соответствующую систему аксиом в логике первого порядка, а также показал её разрешимость.

Аксиомы

Язык арифметики Пресбургера включает константы 0, 1, одну операцию + и предикат равенства =. Аксиомы имеют вид:

  1. ¬(0 = x + 1)
  2. x + 1 = y + 1 x = y
  3. x + 0 = x
  4. (x + y) + 1 = x + (y + 1)
  5. (P(0) (P(x)→P(x + 1))) → P(y), где P — формула первого порядка включающая 0, 1, +, = и одну свободную переменную x.

Следует заметить, что (5) на самом деле не одна аксиома, а схема аксиом, представляющая бесконечное множество аксиом, по одной, для каждой формулы P. (5) является формализацией принципа математической индукции. Она не может быть эквивалентно заменена никакой конечной системой аксиом. Таким образом арифметика Пресбургера не является конечно аксиоматизируемой.

См. также

Литература

  • Cooper, D. C., 1972, «Theorem Proving in Arithmetic without Multiplication» in B. Meltzer and D. Michie, eds., Machine Intelligence. Edinburgh University Press: 91-100.
  • 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 (Apr. 1978). "A simplifier based on efficient decision algorithms". Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 141—150. Проверьте дату в |year= (справка на английском)
  • 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.
  • Pugh, William, 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.
  • Верещагин, Шень. Лекции по математической логике и теории алгоритмов. — МЦНМО, 2002.

Ссылки

  • Online-Proofer Java-апплет, проверяющий формулы арифметики Пресбургера на истинность.  (нем.)

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .




Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2024
WikiSort.ru - проект по пересортировке и дополнению контента Википедии