| dbo:abstract
|
- En ciencias de la computación y lógica matemática, el problema de las teorías de satisfacibilidad módulo (SMT por sus siglas del inglés satisfiability modulo theories) es un problema de decisión para fórmulas lógicas con respecto a las combinaciones de teorías subyacentes expresadas en la lógica de primer orden clásica con igualdad. Ejemplos de teorías usadas comúnmente en ciencias de la computación son la teoría de los números reales, la teoría de los enteros, y las teorías sobre diversas estructuras de datos como listas, arrays, y demás. Los SMT se pueden ver como una forma del problema de satisfacción de restricciones (CSP) y por tanto crear una aproximación formalizada hacia la programación con restricciones. (es)
- In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality (often disallowing quantifiers). SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing. Since Boolean satisfiability is already NP-complete, the SMT problem is typically NP-hard, and for many theories it is undecidable. Researchers study which theories or subsets of theories lead to a decidable SMT problem and the computational complexity of decidable cases. The resulting decision procedures are often implemented directly in SMT solvers; see, for instance, the decidability of Presburger arithmetic. SMT can be thought of as a constraint satisfaction problem and thus a certain formalized approach to constraint programming. (en)
- En informatique et en logique mathématique, un problème de satisfiabilité modulo des théories (SMT) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symboles de prédicat et/ou certaines fonctions. Des exemples de théories incluent la théorie des nombres réels, la théorie de l’arithmétique linéaire, des théories de diverses structures de données comme les listes, les tableaux ou les tableaux de bits, ainsi que des combinaisons de celles-ci. (fr)
- Satisfierbarhet modulo teorier (SMT) är en formaliserad utökning av logiska formler inom datavetenskap och matematisk logik. Ett SMT-problem uppkommer genom att man kombinerar första ordningens logik och likhet med relationer mellan symboler, där tolkningen av både relationerna och symbolerna är godtyckliga och definieras av den logiska teori de tillhör. Exempel på teorier som ofta används inom datavetenskap är teorierna om reella tal och om heltal, som kan användas till exempel för att uttrycka ekvationer över tal med okända variabler. Själva problemet SMT handlar om att ge en tilldelning till dessa symboler så att alla villkor är uppfyllda. På det sättet kan SMT beskrivas som en av flera formaliseringar av villkorsprogrammering. Mer specialiserade teorier är de om olika datastrukturer såsom listor, matriser, bitvektorer, strängar och så vidare. (sv)
- Задача выполнимости формул в теориях (англ. satisfiability modulo theories, SMT) — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для SMT-формул являются: теории целых и вещественных чисел, теории списков, массивов, битовых векторов и т. п. (ru)
- У програмуванні, Satisfiability Modulo Theories (SMT) — це задача для логічних формул з урахуванням теорій, які лежать в їх основі. Прикладами таких теорій для SMT формул є: теорії цілих та дійсних чисел, теорії списків, масивів, бітових векторів та ін. (uk)
|
| rdfs:comment
|
- En ciencias de la computación y lógica matemática, el problema de las teorías de satisfacibilidad módulo (SMT por sus siglas del inglés satisfiability modulo theories) es un problema de decisión para fórmulas lógicas con respecto a las combinaciones de teorías subyacentes expresadas en la lógica de primer orden clásica con igualdad. Ejemplos de teorías usadas comúnmente en ciencias de la computación son la teoría de los números reales, la teoría de los enteros, y las teorías sobre diversas estructuras de datos como listas, arrays, y demás. Los SMT se pueden ver como una forma del problema de satisfacción de restricciones (CSP) y por tanto crear una aproximación formalizada hacia la programación con restricciones. (es)
- En informatique et en logique mathématique, un problème de satisfiabilité modulo des théories (SMT) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symboles de prédicat et/ou certaines fonctions. Des exemples de théories incluent la théorie des nombres réels, la théorie de l’arithmétique linéaire, des théories de diverses structures de données comme les listes, les tableaux ou les tableaux de bits, ainsi que des combinaisons de celles-ci. (fr)
- Задача выполнимости формул в теориях (англ. satisfiability modulo theories, SMT) — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для SMT-формул являются: теории целых и вещественных чисел, теории списков, массивов, битовых векторов и т. п. (ru)
- У програмуванні, Satisfiability Modulo Theories (SMT) — це задача для логічних формул з урахуванням теорій, які лежать в їх основі. Прикладами таких теорій для SMT формул є: теорії цілих та дійсних чисел, теорії списків, масивів, бітових векторів та ін. (uk)
- In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality (often disallowing quantifiers). SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program (en)
- Satisfierbarhet modulo teorier (SMT) är en formaliserad utökning av logiska formler inom datavetenskap och matematisk logik. Ett SMT-problem uppkommer genom att man kombinerar första ordningens logik och likhet med relationer mellan symboler, där tolkningen av både relationerna och symbolerna är godtyckliga och definieras av den logiska teori de tillhör. Exempel på teorier som ofta används inom datavetenskap är teorierna om reella tal och om heltal, som kan användas till exempel för att uttrycka ekvationer över tal med okända variabler. Själva problemet SMT handlar om att ge en tilldelning till dessa symboler så att alla villkor är uppfyllda. På det sättet kan SMT beskrivas som en av flera formaliseringar av villkorsprogrammering. (sv)
|
