Uninterpreted function

Last updated

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.

Contents

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.

See also

Notes

    Related Research Articles

    In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

    The P versus NP problem is a major unsolved problem in theoretical computer science. In informal terms, it asks whether every problem whose solution can be quickly verified can also be quickly solved.

    In mathematics and computer science, the Entscheidungsproblem is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms.

    In mathematics, a Boolean ringR is a ring for which x2 = x for all x in R, that is, a ring that consists only of idempotent elements. An example is the ring of integers modulo 2.

    In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.

    <span class="mw-page-title-main">Model checking</span> Computer science field

    In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

    <span class="mw-page-title-main">Theoretical computer science</span> Subfield of computer science and mathematics

    Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.

    In mathematics, an expression or mathematical expression is a finite combination of symbols that is well-formed according to rules that depend on the context. Mathematical symbols can designate numbers (constants), variables, operations, functions, brackets, punctuation, and grouping to help determine order of operations and other aspects of logical syntax.

    In calculus, symbolic integration is the problem of finding a formula for the antiderivative, or indefinite integral, of a given function f(x), i.e. to find a differentiable function F(x) such that

    <span class="mw-page-title-main">DPLL algorithm</span>

    In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.

    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 involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

    <span class="mw-page-title-main">Boolean circuit</span> Model of computation

    In computational complexity theory and circuit complexity, a Boolean circuit is a mathematical model for combinational digital logic circuits. A formal language can be decided by a family of Boolean circuits, one circuit for each possible input length.

    Logic optimization is a process of finding an equivalent representation of the specified logic circuit under one or more specified constraints. This process is a part of a logic synthesis applied in digital electronics and integrated circuit design.

    In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi-Elgot-Trakhtenbrot theorem gives a logical characterization of the regular languages.

    A solver is a piece of mathematical software, possibly in the form of a stand-alone computer program or as a software library, that 'solves' a mathematical problem. A solver takes problem descriptions in some sort of generic form and calculates their solution. In a solver, the emphasis is on creating a program or library that can easily be applied to other problems of similar type.

    In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not.

    In mathematical logic, computational complexity theory, and computer science, the existential theory of the reals is the set of all true sentences of the form

    Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions.

    In computer science, DPLL(T) is a framework for determining the satisfiability of SMT problems. The algorithm extends the original SAT-solving DPLL algorithm with the ability to reason about an arbitrary theory T. At a high level, the algorithm works by transforming an SMT problem into a SAT formula where atoms are replaced with Boolean variables. The algorithm repeatedly finds a satisfying valuation for the SAT problem, consults a theory solver to check consistency under the domain-specific theory, and then (if a contradiction is found) refines the SAT formula with this information.

    Z3, also known as the Z3 Theorem Prover, is a cross-platform satisfiability modulo theories (SMT) solver by Microsoft.

    References

    1. ↑ Bryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A. (2002). "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2404. pp. 78–92. doi:10.1007/3-540-45657-0_7. ISBN   978-3-540-43997-4. S2CID   9471360.
    2. ↑ Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN   978-0-521-77920-3.
    3. ↑ de Moura, Leonardo; Bjørner, Nikolaj (2009). Formal methods : foundations and applications : 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 : revised selected papers (PDF). Berlin: Springer. ISBN   978-3-642-10452-7.
    This page is based on this Wikipedia article
    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.