Uninterpreted function: Difference between revisions

Revision as of 14:28, 29 January 2015

Revision as of 15:56, 27 February 2016

Line 1:

{{Context|date=October 2009}}

In [[mathematical logic]], an '''uninterpreted function'''<ref>Bryant, Lahiri, Seshia (2002) "Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions". ''Computer Aided Verification'' '''2404/2002''', 106&ndash;122.</ref> or '''function symbol'''<ref>{{cite book|author1=[[Franz Baader]]|author2=[[Tobias Nipkow]]|title=Term Rewriting and All That|year=1999|publisher=Cambridge University Press|isbn=978-0-521-77920-3|pages=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 [[E-Unification]] and [[Narrowing (computer science)|Narrowing]].