HTML Microdata document

This HTML5 document contains 68 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
dct	http://purl.org/dc/terms/
yago-res	http://yago-knowledge.org/resource/
dbo	http://dbpedia.org/ontology/
foaf	http://xmlns.com/foaf/0.1/
n18	https://global.dbpedia.org/id/
yago	http://dbpedia.org/class/yago/
dbt	http://dbpedia.org/resource/Template:
rdfs	http://www.w3.org/2000/01/rdf-schema#
freebase	http://rdf.freebase.com/ns/
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
owl	http://www.w3.org/2002/07/owl#
wikipedia-en	http://en.wikipedia.org/wiki/
dbc	http://dbpedia.org/resource/Category:
dbp	http://dbpedia.org/property/
prov	http://www.w3.org/ns/prov#
xsdh	http://www.w3.org/2001/XMLSchema#
wikidata	http://www.wikidata.org/entity/
gold	http://purl.org/linguistics/gold/
dbr	http://dbpedia.org/resource/

Statements

Subject Item: dbr:Path_ordering_(term_rewriting)
rdf:type: yago:Artifact100021939 yago:PhysicalEntity100001930 dbo:Eukaryote yago:Object100002684 yago:Whole100003553 yago:WikicatRewritingSystems yago:System104377057 yago:Instrumentality103575240
rdfs:label: Path ordering (term rewriting)
rdfs:comment: In theoretical computer science, in particular in term rewriting, a path ordering is a well-founded strict total order (>) on the set of all terms such that f(...) > g(s1,...,sn) if f .> g and f(...) > si for i=1,...,n, where (.>) is a user-given total precedence order on the set of all function symbols. Intuitively, a term f(...) is bigger than any term g(...) built from terms si smaller than f(...) using alower-precedence root symbol g.In particular, by structural induction, a term f(...) is bigger than any term containing only symbols smaller than f. The latter variations include:
dct:subject: dbc:Order_theory dbc:Rewriting_systems
dbo:wikiPageID: 42973489
dbo:wikiPageRevisionID: 1119587803
dbo:wikiPageWikiLink: dbr:Veblen_function dbr:Ackermann_function dbc:Rewriting_systems dbr:Termination_(term_rewriting) dbr:Structural_induction dbr:Reflexive_closure dbr:Well-founded dbr:Wilhelm_Ackermann dbc:Order_theory dbr:Term_(logic) dbr:Successor_function dbr:Reduction_ordering dbr:Strict_total_order dbr:Higher-order_function dbr:Multiset dbr:Continuous_function_(set_theory) dbr:Term_rewriting dbr:Elementary_algebra dbr:General_recursive_function dbr:Irreflexive dbr:Transitive_relation dbr:Knuth–Bendix_completion_algorithm dbr:Theoretical_computer_science dbr:Lexicographical_order dbr:Ackermann_ordinal
owl:sameAs: yago-res:Path_ordering_(term_rewriting) wikidata:Q18386969 freebase:m.010rz80_ n18:n1zy
dbp:wikiPageUsesTemplate: dbt:Su dbt:Reflist dbt:Redirect
dbp:b: i=0
dbo:abstract: In theoretical computer science, in particular in term rewriting, a path ordering is a well-founded strict total order (>) on the set of all terms such that f(...) > g(s1,...,sn) if f .> g and f(...) > si for i=1,...,n, where (.>) is a user-given total precedence order on the set of all function symbols. Intuitively, a term f(...) is bigger than any term g(...) built from terms si smaller than f(...) using alower-precedence root symbol g.In particular, by structural induction, a term f(...) is bigger than any term containing only symbols smaller than f. A path ordering is often used as reduction ordering in term rewriting, in particular in the Knuth–Bendix completion algorithm.As an example, a term rewriting system for "multiplying out" mathematical expressions could contain a rule x*(y+z) → (x*y) + (x*z). In order to prove termination, a reduction ordering (>) must be found with respect to which the term x*(y+z) is greater than the term (x*y)+(x*z). This is not trivial, since the former term contains both fewer function symbols and fewer variables than the latter. However, setting the precedence (*) .> (+), a path ordering can be used, since both x*(y+z) > x*y and x*(y+z) > x*z is easy to achieve. There may also be systems for certain general recursive functions, for example a system for the Ackermann function may contain the rule A(a+, b+) → A(a, A(a+, b)), where b+ denotes the successor of b. Given two terms s and t, with a root symbol f and g, respectively, to decide their relation their root symbols are compared first. * If f <. g, then s can dominate t only if one of s's subterms does. * If f .> g, then s dominates t if s dominates each of t's subterms. * If f = g, then the immediate subterms of s and t need to be compared recursively. Depending on the particular method, different variations of path orderings exist. The latter variations include: * the multiset path ordering (mpo), originally called recursive path ordering (rpo) * the lexicographic path ordering (lpo) * a combination of mpo and lpo, called recursive path ordering by Dershowitz, Jouannaud (1990) Dershowitz, Okada (1988) list more variants, and relate them to Ackermann's system of ordinal notations. In particular, an upper bound given on the order types of recursive path orderings with n function symbols is φ(n,0), using Veblen's function for large countable ordinals.
gold:hypernym: dbr:Order
prov:wasDerivedFrom: wikipedia-en:Path_ordering_(term_rewriting)?oldid=1119587803&ns=0
dbo:wikiPageLength: 7642
foaf:isPrimaryTopicOf: wikipedia-en:Path_ordering_(term_rewriting)

Subject Item: dbr:MPO_(term_rewriting)
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)
dbo:wikiPageRedirects: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:Rewriting
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:Nachum_Dershowitz
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:Recursive_path_ordering
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)
dbo:wikiPageRedirects: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:LPO_(term_rewriting)
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)
dbo:wikiPageRedirects: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:Multiset_path_ordering
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)
dbo:wikiPageRedirects: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:Lexicographic_path_ordering
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)
dbo:wikiPageRedirects: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:Veblen_function
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)

Subject Item: dbr:RPO_(term_rewriting)
dbo:wikiPageWikiLink: dbr:Path_ordering_(term_rewriting)
dbo:wikiPageRedirects: dbr:Path_ordering_(term_rewriting)

Subject Item: wikipedia-en:Path_ordering_(term_rewriting)
foaf:primaryTopic: dbr:Path_ordering_(term_rewriting)