| dbo:abstract
|
- In mathematical logic, a first-order language of the real numbers is the set of all well-formed sentences of first-order logic that involve universal and existential quantifiers and logical combinations of equalities and inequalities of expressions over real variables. The corresponding first-order theory is the set of sentences that are actually true of the real numbers. There are several different such theories, with different expressive power, depending on the primitive operations that are allowed to be used in the expression. A fundamental question in the study of these theories is whether they are decidable: that is, is there an algorithm that can take a sentence as input and produce as output an answer "yes" or "no" to the question of whether the sentence is true in the theory. The theory of real closed fields is the theory in which the primitive operations are multiplication and addition; this implies that, in this theory, the only numbers that can be defined are the real algebraic numbers. As proven by Tarski, this theory is decidable; see Tarski–Seidenberg theorem and Quantifier elimination. Current implementations of decision procedures for the theory of real closed fields are often based on quantifier elimination by cylindrical algebraic decomposition. Tarski's exponential function problem concerns the extension of this theory to another primitive operation, the exponential function. It is an open problem whether this theory is decidable, but if Schanuel's conjecture holds then the decidability of this theory would follow. In contrast, the extension of the theory of real closed fields with the sine function is undecidable since this allows encoding of the undecidable theory of integers (see Richardson's theorem). Still, one can handle the undecidable case with functions such as sine by using algorithms that do not necessarily terminate always. In particular, one can design algorithms that are only required to terminate for input formulas that are robust, that is, formulas whose satisfiability does not change if the formula is slightly perturbed. Alternatively, it is also possible to use purely heuristic approaches. (en)
- Алгоритм Тарского — универсальный алгоритм, позволяющий установить истинность или ложность любой замкнутой арифметической формулы первого порядка с переменными для вещественных чисел.Основан на теореме Зайденберга — Тарского. Алгоритм Тарского позволяет проверить истинность или ложность любого высказывания о конечном количестве вещественных чисел. Такое высказывание можно записать на стандартном языке математической логики первого порядка. С помощью введения декартовых координат к подобному виду можно привести, например, любую задачу евклидовой геометрии — что в принципе позволяет автоматически доказывать любую теорему элементарной геометрии. Следует отметить, что для аналогичного языка с переменными, принимающими только рациональные значения, алгоритм, подобный алгоритму Тарского, невозможен. (ru)
- Алгоритм Тарського — універсальний алгоритм, що дозволяє встановити істинність або хибність будь-якої замкнутої арифметичної формули першого порядку зі змінними для дійсних чисел. Алгоритм Тарського дозволяє перевірити істинність або хибність будь-якого висловлювання про кінцеву кількість дійсних чисел. Таке висловлювання можна записати на стандартній мові математичної логіки першого порядку. За допомогою введення декартових координат до подібного виду можна навести, наприклад, будь-яку задачу евклідової геометрії — що дозволяє автоматично доводити будь-яку теорему елементарної геометрії. Варто зазначити, що для аналогічної мови зі змінними, які приймають лише раціональні значення, алгоритм, подібний алгоритму Тарського, неможливий. (uk)
|
| rdfs:comment
|
- In mathematical logic, a first-order language of the real numbers is the set of all well-formed sentences of first-order logic that involve universal and existential quantifiers and logical combinations of equalities and inequalities of expressions over real variables. The corresponding first-order theory is the set of sentences that are actually true of the real numbers. There are several different such theories, with different expressive power, depending on the primitive operations that are allowed to be used in the expression. A fundamental question in the study of these theories is whether they are decidable: that is, is there an algorithm that can take a sentence as input and produce as output an answer "yes" or "no" to the question of whether the sentence is true in the theory. (en)
- Алгоритм Тарского — универсальный алгоритм, позволяющий установить истинность или ложность любой замкнутой арифметической формулы первого порядка с переменными для вещественных чисел.Основан на теореме Зайденберга — Тарского. Следует отметить, что для аналогичного языка с переменными, принимающими только рациональные значения, алгоритм, подобный алгоритму Тарского, невозможен. (ru)
- Алгоритм Тарського — універсальний алгоритм, що дозволяє встановити істинність або хибність будь-якої замкнутої арифметичної формули першого порядку зі змінними для дійсних чисел. Алгоритм Тарського дозволяє перевірити істинність або хибність будь-якого висловлювання про кінцеву кількість дійсних чисел. Таке висловлювання можна записати на стандартній мові математичної логіки першого порядку. За допомогою введення декартових координат до подібного виду можна навести, наприклад, будь-яку задачу евклідової геометрії — що дозволяє автоматично доводити будь-яку теорему елементарної геометрії. (uk)
|
