In computer science, Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on.

PropertyValue
dbpprop:abstract
  • In computer science, Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on.
  • Problème SMT (Satisfiability Modulo Theories) est un problème de la décision pour les formules logiques dans le respect d'une théorie exprimée dans la logique du premier ordre contenant l'égalité. Des exemples de théories sont la théorie des nombres réels, la théorie de entiers linéaires, et des théories d'une variété de structures de données comme les listes, les tableaux, les vecteurs de bits, etc.
dbpprop:harvProperty
  • Bauer
  • Fränzle
  • Herde
  • Nieuwenhuis
  • Oliveras
  • Pister
  • Ratschan
  • Schubert
  • Tautschnig
  • Tinelli
  • 2006 (xsd:integer)
  • 2007 (xsd:integer)
dbpprop:hasPhotoCollection
dbpprop:reference
dbpprop:relatedInstance
dbpprop:wikiPageUsesTemplate
rdf:type
rdfs:comment
  • In computer science, Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on.
  • Problème SMT (Satisfiability Modulo Theories) est un problème de la décision pour les formules logiques dans le respect d'une théorie exprimée dans la logique du premier ordre contenant l'égalité. Des exemples de théories sont la théorie des nombres réels, la théorie de entiers linéaires, et des théories d'une variété de structures de données comme les listes, les tableaux, les vecteurs de bits, etc.
rdfs:label
  • Satisfiability Modulo Theories
  • Satisfiability Modulo Theories (SMT)
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of
is owl:sameAs of