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
Example
As an example of uninterpreted functions for
(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
See also
Notes
References
- S2CID 9471360.
- ISBN 978-0-521-77920-3.
- ISBN 978-3-642-10452-7.
| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory |
| ||||||||
| Computability theory | |||||||||
| Related | |||||||||
 | This formal methods-related article is a stub. You can help Wikipedia by expanding it. |