mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...

, an uninterpreted function or function symbol is one that has no other property than its name and ''

n-ary -ary may refer to: * The arity of a function, operation, or relation ** -ary associativity, a specific rule attached to -ary functions *** -ary group, a generalization of group * The radix of a numerical representation system * The number of le ...

'' 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 In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. Informally, a free object over a set ''A'' can be thought of as being a "generic" algebraic structure over ''A'': the only equations that hold between ele ...

, or the empty theory, being the

theory A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be s ...

having an empty set of

sentences ''The Four Books of Sentences'' (''Libri Quattuor Sententiarum'') is a book of theology written by Peter Lombard in the 12th century. It is a systematic compilation of theology, written around 1150; it derives its name from the ''sententiae'' o ...

(in analogy to an

initial algebra In mathematics, an initial algebra is an initial object in the category of -algebras for a given endofunctor . This initiality provides a general framework for induction and recursion. Examples Functor Consider the endofunctor sending t ...

). Theories with a non-empty set of equations are known as

equational theories Equational may refer to: * Equative, a construction in linguistics * something pertaining to equations, in mathematics * something pertaining to equality, in logic See also * * Equation (disambiguation) * Equality (disambiguation) Equality m ...

. The

satisfiability In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...

problem for free theories is solved by syntactic unification; algorithms for the latter are used by interpreters for various computer languages, such as

Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...

. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see

Unification (computer science) In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. Depending on which expressions (also called ''terms'') are allowed to occur in an equation set (also called ''unification prob ...

Example

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

SMT solver In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...

: (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 A signature (; from la, signare, "to sign") is a handwritten (and often stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. The writer of a ...

), 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 In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm whethe ...

for free theories is particularly important, because many theories can be reduced by it. Free theories can be solved by searching for

common subexpression Common may refer to: Places * Common, a townland in County Tyrone, Northern Ireland * Boston Common, a central public park in Boston, Massachusetts * Cambridge Common, common land area in Cambridge, Massachusetts * Clapham Common, originally com ...

s to form the

congruence closure In mathematics, a subset of a given set is closed under an operation of the larger set if performing that operation on members of the subset always produces a member of that subset. For example, the natural numbers are closed under addition, bu ...

. Solvers include

satisfiability modulo theories In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...

solvers.

Notes

References

{{Formalmethods-stub Specification languages