SMT

E904155

field of study subfield of computer science subfield of mathematical logic

SMT is a field in computer science and mathematical logic that studies the satisfiability of logical formulas with respect to background theories such as arithmetic, arrays, and bit-vectors.

Try in SPARQL Jump to: Statements Referenced by

Statements (48)

Predicate	Object
instanceOf	field of study ⓘ subfield of computer science ⓘ subfield of mathematical logic ⓘ
algorithmicTechnique	DPLL(T) NERFINISHED ⓘ Nelson–Oppen combination NERFINISHED ⓘ conflict-driven clause learning in theories ⓘ theory propagation ⓘ
appliesToTheory	algebraic datatypes ⓘ arithmetic ⓘ arrays ⓘ bit-vectors ⓘ data structures ⓘ floating-point arithmetic ⓘ linear arithmetic ⓘ nonlinear arithmetic ⓘ strings ⓘ uninterpreted functions ⓘ
extends	SAT NERFINISHED ⓘ
focusesOn	background theories ⓘ
fullName	Satisfiability Modulo Theories NERFINISHED ⓘ
goal	decide satisfiability of formulas in background theories ⓘ
hasApplication	automated reasoning ⓘ bounded model checking ⓘ constraint-based program analysis ⓘ optimization modulo theories ⓘ path feasibility checking ⓘ symbolic execution ⓘ
hasCommunity	SMT-COMP NERFINISHED ⓘ
hasStandard	SMT-LIB NERFINISHED ⓘ SMT-LIB 2 NERFINISHED ⓘ
hasTool	SMT solver ⓘ
relatedTo	SAT NERFINISHED ⓘ constraint satisfaction ⓘ decision procedures ⓘ propositional satisfiability ⓘ theorem proving ⓘ
studies	satisfiability of logical formulas ⓘ
typicalInput	formulas with quantifiers ⓘ quantifier-free formulas ⓘ
usedIn	constraint solving ⓘ formal verification ⓘ hardware verification ⓘ model checking ⓘ program analysis ⓘ software verification ⓘ synthesis ⓘ test generation ⓘ
uses	first-order logic ⓘ

Referenced by (1)

Full triples — surface form annotated when it differs from this entity's canonical label.

Satisfiability Modulo Theories (SMT) → abbreviation → SMT ⓘ

subject surface form: Satisfiability Modulo Theories