Uninterpreted function: Difference between revisions

Revision as of 04:20, 11 June 2011

Revision as of 15:52, 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'''' is one that has no other property than its name and arity. They areFunction oftensymbols are used, together with equalityconstants inand formal reasoningvariables, especiallyto form using[[term computers(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 particularly important, as many other theories can be reduced to it.

Line 31:

==References==

{{Reflist}}

{{Formalmethods-stub}}