Presburger Arithmetic

定义 Definition

Presburger arithmetic（普雷斯伯格算术）是数理逻辑中的一个形式理论，描述只包含加法的整数（或自然数）算术。通常允许使用常数（如 0、1）、加法、相等号，以及逻辑量词（∀、∃），但不允许乘法（乘法若加入一般会导致理论复杂度大幅上升）。它以“可判定”（存在算法判断任意给定公式是否为真/可满足）而著名。

例句 Examples

Presburger arithmetic can express constraints like \(x + y = 10\), but not \(x \times y = 10\).
普雷斯伯格算术可以表达像 \(x + y = 10\) 这样的约束，但不能表达 \(x \times y = 10\)。

In formal verification, some properties of programs are reduced to Presburger arithmetic so that satisfiability can be decided automatically.
在形式化验证中，程序的一些性质会被化归为普雷斯伯格算术，从而可以自动判定其可满足性。

发音 Pronunciation

/ˈprɛz.bɝː.ɡər əˈrɪθ.mə.tɪk/

词源 Etymology

该术语来自波兰逻辑学家 Mojżesz Presburger（莫伊谢什·普雷斯伯格）的姓氏。他在 1929 年的论文中提出并研究了“只含加法”的算术体系，证明其重要的可判定性等性质，因此后人将该体系称为 Presburger arithmetic。

相关词 Related Words

• Arithmetic
• Logic
• Model Theory
• Decidability
• Quantifier
• First-Order Logic
• Peano Arithmetic
• Skolem Arithmetic

文学与著作中的用例 Literary Works

• Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen（Presburger, 1929）
• Model Theory（C. C. Chang & H. J. Keisler）
• Logic in Computer Science: Modelling and Reasoning about Systems（Michael Huth & Mark Ryan）
• Introduction to Automata Theory, Languages, and Computation（Hopcroft, Motwani, Ullman）