Content deleted Content added
Harrylime1 (talk | contribs) No edit summary |
m WP:ADOPTYPO boolean -> Boolean |
||
| (5 intermediate revisions by 5 users not shown) | |||
Line 1:
{{Short description|Type of function in mathematical logic}}
In [[mathematical logic]], an '''uninterpreted function'''<ref>{{Cite book | chapter-url=https://link.springer.com/content/pdf/10.1007/3-540-45657-0_7.pdf |doi = 10.1007/3-540-45657-0_7|chapter = Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions|title = Computer Aided Verification|volume = 2404|pages = 78–92|series = Lecture Notes in Computer Science|year = 2002|last1 = Bryant|first1 = Randal E.|last2 = Lahiri|first2 = Shuvendu K.|last3 = Seshia|first3 = Sanjit A.|isbn = 978-3-540-43997-4| s2cid=9471360 }}</ref> or '''function symbol'''<ref>{{cite book |last1=Baader |first1=Franz |authorlink1=Franz Baader |last2=Nipkow |first2=Tobias |authorlink2=Tobias Nipkow |year=1999 |title=Term Rewriting and All That |publisher=Cambridge University Press |isbn=978-0-521-77920-3 |page=34}}</ref> is one that has no other property than its name and ''[[Arity|n-ary]]'' form. Function symbols are used, together with constants and variables, to form [[term (logic)|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 (mathematical logic)|theory]] having an empty set of [[sentence (mathematical logic)|sentences]] (in analogy to an [[initial algebra]]). Theories with a non-empty set of equations are known as [[equational theory|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 [[
==Example==
As an example of uninterpreted functions for [[SMT-LIB]], if this input is given to an [[Satisfiability modulo theories|SMT solver]]:
<syntaxhighlight lang="text" line="1">
(declare-fun f (Int) Int)
Line 22:
The [[decision problem]] for free theories is particularly important, because many theories can be reduced by it.<ref>{{cite book |last1=de Moura |first1=Leonardo |last2=Bjørner |first2=Nikolaj |title=Formal methods : foundations and applications : 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 : revised selected papers |date=2009 |publisher=Springer |___location=Berlin |isbn=978-3-642-10452-7 |url=https://leodemoura.github.io/files/sbmf09.pdf}}</ref>
Free theories can be solved by searching for [[common subexpression]]s to form the [[congruence closure]].{{clarify|reason=Indicate about solving which problem in free theories the sentence is supposed to speak. E.g. to solve the satisfiability problem of conjunctions of equations, the Martelli-Montanari syntactic unification algorithm suffices, neither common subexpressions nor congruence closures are needed. Maybe, satisfiability of arbitrary
== See also ==
| |||