Uninterpreted function

<h2 id="example">Example</h2>
<p>As an example of uninterpreted functions for <a href="/facts/SMT-LIB/10mBFLFB">SMT-LIB</a>, if this input is given to an <a href="/facts/Satisfiability_modulo_theories/10mBFLFB">SMT solver</a>:
</p>
(declare-fun f (Int) Int)
(assert (= (f 10) 1))

<p>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 <a href="/facts/Signature_(logic)/C0YQCuce">signature</a>), so it is possible that f(10) = 1. But by applying the input below:
</p>
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(assert (= (f 10) 42))

<p>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.
</p>
<h2 id="discussion">Discussion</h2>
<p>The <a href="/facts/Decision_problem/cQNWjbdE">decision problem</a> for free theories is particularly important, because many theories can be reduced by it.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a>
</p><p>Free theories can be solved by searching for <a href="/facts/Common_subexpression/hlCW19QS">common subexpressions</a> to form the <a href="/facts/Congruence_closure/Ct6r2fJz">congruence closure</a>. Solvers include <a href="/facts/Satisfiability_modulo_theories/10mBFLFB">satisfiability modulo theories</a> solvers.
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Algebraic_data_type/Fn9KhnAb">Algebraic data type</a></li>
<li><a href="/facts/Initial_algebra/KbryBRxs">Initial algebra</a></li>
<li><a href="/facts/Term_algebra/kRGlTKMq">Term algebra</a></li>
<li><a href="/facts/Theory_of_pure_equality/lf3LRWtY">Theory of pure equality</a></li></ul>
<h2 id="notes">Notes</h2>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>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. <a href="978-3-540-43997-4" target="_blank">978-3-540-43997-4</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3. <a href="978-0-521-77920-3" target="_blank">978-0-521-77920-3</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>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. <a href="978-3-642-10452-7" target="_blank">978-3-642-10452-7</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
</ol>

Uninterpreted function open-in-new

Uninterpreted function