Uninterpreted function: Difference between revisions

Revision as of 15:56, 13 June 2011

Revision as of 16:12, 13 June 2011

Line 3:

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''', 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]]),. and thusTheories with a non-empty set of equations are known as [[freeequational objecttheory|freeequational theories]]. The [[decision problem]] for free theories is knowna as[[satisfiability]] problem, and is solved by [[syntactic unification]],. andIt is particularly important, as many other theories can be reduced to it. Interpreters for various computer languages, such as [[Prolog]], require algorithms for solving the free theory.

==Example==