You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

7 lines
512 B

The satisfiability modulo theories (SMT) problem refers
to the problem of determining whether a formula in predicate logic is satisfiable
with respect to some theory. A theory fixes the interpretation/meaning of certain
predicate and function symbols. Checking whether a formula in predicate logic is
satisfiable with respect to a theory means that we are not interested in arbitrary
models but in models that interpret the functions and predicates contained in
the theory as defined by the axioms in the theory.