Uninterpreted function
In mathematical logic, an uninterpreted function or function symbol is one that has no other property than its name and n-ary form. Function symbols are used, together with constants and variables, to form terms.
- Comment
- enIn mathematical logic, an uninterpreted function or function symbol is one that has no other property than its name and n-ary form. Function symbols are used, together with constants and variables, to form terms.
- Date
- enMay 2014
- Has abstract
- enIn mathematical logic, an uninterpreted function or function symbol is one that has no other property than its name and n-ary form. Function symbols are used, together with constants and variables, to form 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 having an empty set of sentences (in analogy to an initial algebra). Theories with a non-empty set of equations are known as 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 Unification (computer science).
- Is primary topic of
- Uninterpreted function
- Label
- enUninterpreted function
- Link from a Wikipage to another Wikipage
- Algebraic data type
- Arity
- Category:Specification languages
- Common subexpression
- Congruence closure
- Decision problem
- Equational theory
- Free object
- Initial algebra
- Mathematical logic
- Prolog
- Satisfiability
- Satisfiability modulo theories
- Sentence (mathematical logic)
- Signature (logic)
- Syntactic unification
- Term (logic)
- Term algebra
- Theory (mathematical logic)
- Theory of pure equality
- Unification (computer science)
- Reason
- enIndicate about solving which problem in free theories the sentence is supposed to speak. E.g. to solve the satisfiability problem of conjunctions of equations, the Martelli-Montanari syntactic unification algorithm suffices, neither common subexpressions nor congruence closures are needed. Maybe, satisfiability of arbitrary boolean combinations of equations is meant?
- SameAs
- 4wner
- m.05zkr99
- Q7885264
- Uninterpreted function
- تابع تفسیرنشده
- Subject
- Category:Specification languages
- WasDerivedFrom
- Uninterpreted function?oldid=1122711870&ns=0
- WikiPageLength
- 4005
- Wikipage page ID
- 22542131
- Wikipage revision ID
- 1122711870
- WikiPageUsesTemplate
- Template:Clarify
- Template:Formalmethods-stub
- Template:Mathematical logic
- Template:Reflist