# Uninterpreted function

In mathematical logic, an **uninterpreted function**^{[1]} or **function symbol**^{[2]} is one that has no other property than its name and *n-ary* form. Function symbols are used, together with constants and variables, to form terms.

The **theory of uninterpreted functions** is also sometimes called the **free theory**, because it is freely generated, and thus a free object, or the **empty theory**, being the theory having an empty set of sentences (in analogy to an initial algebra). Theories with a non-empty set of equations are known as equational theories. The satisfiability problem for free theories is solved by syntactic unification; algorithms for the latter are used by interpreters for various computer languages, such as Prolog. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see Unification (computer science).

## Example

As an example of uninterpreted functions for SMT-LIB, if this input is given to an SMT solver:

```
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
```

the SMT solver would return "This input is satisfiable". That happens because `f`

is an uninterpreted function (i.e., all that is known about `f`

is its signature), so it is possible that `f(10) = 1`

. But by applying the input below:

```
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))
```

the SMT solver would return "This input is unsatisfiable". That happens because `f`

, being a function, can never return different values for the same input.

## Discussion

The decision problem for free theories is particularly important, because many theories can be reduced by it.^{[3]}

Free theories can be solved by searching for common subexpressions to form the congruence closure.^{[clarification needed]} Solvers include satisfiability modulo theories solvers.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.