Content deleted Content added
→References: onw section "Notes" |
→top: there are many decision problems for the free theory, unifications solves the sat. problem; specified/linked statement about 'other theories' |
||
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–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. 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 [[
==Example==
| |||