First order theories

A theory is a collection of constants, functions, and predicates, and formulas that define their behavior, which are called the theory axioms - and often these axioms dictate a particular domain of discourse as well. When we work within a theory, the basics of what we will be describing is pinned down, and we only have to express things that are specific to our problem. A classic example of a theory is the integers. When we work in that theory, the domain of discourse is the integers, the functions are plus, minus and times, the predicates include less-than, the constants base 10 integers, and so on.

Satisfiability Modulo Theory (SMT) Solvers

SMT solvers can find models for formulas in certain theories. This class was all about the activity in which you wrote a program that generated a first order formula in the theory of Linear Integer Arithmetic (ILA), and then used the Z3 SAT solver to find a model, which ultimately provided the solution to a "Subset Sum" problem.