| dbo:abstract
|
- The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix) is a semi-decision algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra. Buchberger's algorithm for computing Gröbner bases is a very similar algorithm. Although developed independently, it may also be seen as the instantiation of Knuth–Bendix algorithm in the theory of polynomial rings. (en)
- La procédure de complétion de Knuth-Bendix ou complétion de Knuth-Bendix (aussi appelée algorithme de Knuth-Bendix ) transforme, si elle réussit, un ensemble fini d'identités (sur des termes) décrivant une structure algébrique en un système de réécriture de termes confluent et qui termine (dit alors convergent). Le processus de complétion a été inventé par Donald Knuthaidé d'un étudiant, nommé Peter Bendix, pour la mise en œuvre. En cas de réussite, la complétion donne un moyen effectif de résoudre le problème du mot pour l'algèbre en question, comme cela a été démontré par Gérard Huet. Par exemple, pour la théorie équationnelle des groupes (voir schéma à droite), la complétion fournit un système de réécriture de terme confluent et qui termine. On peut alors décider si une équation t1 = t2 est vraie dans tous les groupes (même si décider si une formule du premier ordre est vraie dans tous les groupes est indécidable). Malheureusement, le problème du mot étant indécidable en général, la procédure de complétion ne se termine pas toujours avec succès. Elle peut soit s'exécuter indéfiniment, soit échouer en rencontrant une identité non-orientable (qu'elle ne peut pas transformer en règle de réécriture sans être sûre de ne pas mettre en danger la terminaison). Il existe une variante de la procédure de complétion qui n'échoue pas sur les identités non orientables. Elle fournit une procédure de semi-décision pour le problème du mot, autrement dit, elle permet de dire si une identité donnée est déductible des identités qui décrivent l'algèbre en question, dans tous les cas où elle l'est effectivement, mais peut ne jamais terminer. (fr)
- クヌース・ベンディックス完備化アルゴリズム（英: Knuth–Bendix completion algorithm）、あるいはクヌース・ベンディックス完備化手続きは、等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換するアルゴリズムである。このアルゴリズムは普遍代数（en）での語の問題（word problem）（en）を解くための手法としてクヌースとベンディックスから提案された。アルゴリズムは必ず成功するとは限らないが、成功した場合は停止性と合流性のある項書き換えシステムを生成することができる。そのベースとなる考え方は多くの分野で応用することができる。 (ja)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 21397 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:title
|
- Knuth–Bendix Completion Algorithm (en)
|
| dbp:urlname
|
- Knuth-BendixCompletionAlgorithm (en)
|
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix) is a semi-decision algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra. Buchberger's algorithm for computing Gröbner bases is a very similar algorithm. Although developed independently, it may also be seen as the instantiation of Knuth–Bendix algorithm in the theory of polynomial rings. (en)
- クヌース・ベンディックス完備化アルゴリズム（英: Knuth–Bendix completion algorithm）、あるいはクヌース・ベンディックス完備化手続きは、等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換するアルゴリズムである。このアルゴリズムは普遍代数（en）での語の問題（word problem）（en）を解くための手法としてクヌースとベンディックスから提案された。アルゴリズムは必ず成功するとは限らないが、成功した場合は停止性と合流性のある項書き換えシステムを生成することができる。そのベースとなる考え方は多くの分野で応用することができる。 (ja)
- La procédure de complétion de Knuth-Bendix ou complétion de Knuth-Bendix (aussi appelée algorithme de Knuth-Bendix ) transforme, si elle réussit, un ensemble fini d'identités (sur des termes) décrivant une structure algébrique en un système de réécriture de termes confluent et qui termine (dit alors convergent). Le processus de complétion a été inventé par Donald Knuthaidé d'un étudiant, nommé Peter Bendix, pour la mise en œuvre. (fr)
|
| rdfs:label
|
- Knuth–Bendix completion algorithm (en)
- Complétion de Knuth-Bendix (fr)
- クヌース・ベンディックス完備化アルゴリズム (ja)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
