Uninterpreted function: Difference between revisions

Revision as of 15:52, 13 June 2011

Revision as of 15:56, 13 June 2011

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=9780521779203|pages=34}}</ref> is one that has no other property than its name and arity. 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''' or '''empty theory''', being the [[theory (mathematical logic)|theory]] having an empty set of [[sentence (mathematical logic)|sentences]] (in analogy to an [[initial algebra]]), and thus [[free object|free]]. The [[decision problem]] for free theories is known as [[syntactic unification]], and is particularly important, as many other theories can be reduced to it.

==Example==