Definition A generalisation of [[SAT]] theory to more complex formulas including: real numbers integers data structures (arrays, lists)