| dbo:abstract |
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. 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). (en) |
| dbo:wikiPageID |
22542131 (xsd:integer) |
| dbo:wikiPageLength |
4005 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID |
1122711870 (xsd:integer) |
| dbo:wikiPageWikiLink |
dbr:Prolog dbr:Unification_(computer_science) dbr:Decision_problem dbr:Initial_algebra dbr:Mathematical_logic dbr:Congruence_closure dbr:Syntactic_unification dbr:Arity dbr:Algebraic_data_type dbr:Term_(logic) dbc:Specification_languages dbr:Term_algebra dbr:Theory_(mathematical_logic) dbr:Free_object dbr:Satisfiability dbr:Satisfiability_modulo_theories dbr:Sentence_(mathematical_logic) dbr:Signature_(logic) dbr:Theory_of_pure_equality dbr:Equational_theory dbr:Common_subexpression |
| dbp:date |
May 2014 (en) |
| dbp:reason |
Indicate 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? (en) |
| dbp:wikiPageUsesTemplate |
dbt:Clarify dbt:Reflist dbt:Formalmethods-stub dbt:Mathematical_logic |
| dct:subject |
dbc:Specification_languages |
| rdf:type |
yago:WikicatSpecificationLanguages yago:Abstraction100002137 yago:Artifact100021939 yago:Communication100033020 yago:Language106282651 yago:Object100002684 yago:PhysicalEntity100001930 yago:YagoGeoEntity yago:YagoPermanentlyLocatedEntity yago:Structure104341686 yago:Whole100003553 yago:WikicatFreeAlgebraicStructures |
| rdfs:comment |
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. (en) |
| rdfs:label |
Uninterpreted function (en) |
| owl:sameAs |
freebase:Uninterpreted function yago-res:Uninterpreted function wikidata:Uninterpreted function dbpedia-fa:Uninterpreted function https://global.dbpedia.org/id/4wner |
| prov:wasDerivedFrom |
wikipedia-en:Uninterpreted_function?oldid=1122711870&ns=0 |
| foaf:isPrimaryTopicOf |
wikipedia-en:Uninterpreted_function |
| is dbo:wikiPageRedirects of |
dbr:Free_theory dbr:Empty_theory dbr:Function_letter dbr:Function_symbol_(logic) dbr:Uninterpreted_term |
| is dbo:wikiPageWikiLink of |
dbr:Unification_(computer_science) dbr:Free_function dbr:Boolean_satisfiability_problem dbr:Free_theory dbr:Empty_theory dbr:Satisfiability_modulo_theories dbr:Function_letter dbr:Function_symbol_(logic) dbr:Uninterpreted_term |
| is foaf:primaryTopic of |
wikipedia-en:Uninterpreted_function |