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

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

Namespace Prefixes

PrefixIRI
dbpedia-dehttp://de.dbpedia.org/resource/
dcthttp://purl.org/dc/terms/
n20https://commons.wikimedia.org/wiki/File:
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-kkhttp://kk.dbpedia.org/resource/
dbpedia-eshttp://es.dbpedia.org/resource/
n36http://g.co/kg/m/
dbpedia-ruhttp://ru.dbpedia.org/resource/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n25https://blog.cyclonium.com/2020/04/19/unification/
dbpedia-ukhttp://uk.dbpedia.org/resource/
category-frhttp://fr.dbpedia.org/resource/Catégorie:
dbpedia-plhttp://pl.dbpedia.org/resource/
dbpedia-pthttp://pt.dbpedia.org/resource/
n16http://fr.dbpedia.org/resource/Modèle:Boîte_déroulante/
dbpedia-cshttp://cs.dbpedia.org/resource/
n10http://fr.dbpedia.org/resource/Modèle:
n17http://fr.dbpedia.org/resource/Fichier:
n15http://ky.dbpedia.org/resource/
dbpedia-fahttp://fa.dbpedia.org/resource/
n22http://commons.wikimedia.org/wiki/Special:FilePath/
dbpedia-nohttp://no.dbpedia.org/resource/
wikipedia-frhttp://fr.wikipedia.org/wiki/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n29http://mathworld.wolfram.com/
owlhttp://www.w3.org/2002/07/owl#
n33http://ma-graph.org/entity/
dbpedia-vihttp://vi.dbpedia.org/resource/
dbpedia-zhhttp://zh.dbpedia.org/resource/
dbpedia-frhttp://fr.dbpedia.org/resource/
prop-frhttp://fr.dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
dbpedia-bghttp://bg.dbpedia.org/resource/
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/

Statements

Subject Item
dbpedia-fr:Unification
rdfs:label
Unificação Unifikation (Logik) Unification
rdfs:comment
En informatique et en logique, l'unification est un processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques. Par exemple, et peuvent être rendus identiques par la substitution et , qui donne quand on l'applique à chacun de ces termes le terme . Dit autrement, l'unification est la résolution d'une équation dans l'algèbre des termes (unification syntaxique) ou dans une algèbre quotient par un ensemble d'identités (unification modulo une théorie) ; la solution de l'équation est la substitution qui rend les deux termes identiques et que l'on appelle l'unificateur.L'unification a des applications en inférence de types, programmation logique, en démonstration automatique de théorèmes, en système de réécriture, en traitem
rdfs:seeAlso
n20:LL-Q150_(fra)-0x010C-Unification.wav n29:Unification.html
owl:sameAs
dbpedia-es:Unificación_(ciencias_de_la_computación) dbpedia-vi:Hợp_nhất_(phép_toán) dbpedia-uk:Уніфікація_(інформатика) dbpedia-ja:ユニフィケーション dbpedia-fa:همان‌سازی_(علوم_رایانه) dbpedia-zh:合一 n15:Унификация dbr:Unification_(computer_science) dbpedia-de:Unifikation_(Logik) dbpedia-cs:Unifikace_(logika) dbpedia-no:Unifikasjon wikidata:Q609057 dbpedia-pt:Unificação dbpedia-ru:Частный_случай_формулы n33:96146094 dbpedia-kk:Унификация dbpedia-pl:Unifikacja_(informatyka) n36:0f6v3 dbpedia-bg:Унификация_(информатика)
dbo:wikiPageID
19165
dbo:wikiPageRevisionID
187881412
dbo:wikiPageWikiLink
category-fr:Réécriture dbpedia-fr:Algorithme_de_parcours_en_profondeur category-fr:Informatique_théorique n17:John_Alan_Robinson_IMG_0493.jpg dbpedia-fr:Informatique category-fr:Algèbre dbpedia-fr:Réécriture_(informatique) dbpedia-fr:Logique_d'ordre_supérieur dbpedia-fr:Langage_de_programmation dbpedia-fr:Logique dbpedia-fr:Terme_(logique) dbpedia-fr:Union-find dbpedia-fr:John_Alan_Robinson dbpedia-fr:Jacques_Herbrand n17:Unification_animation.gif n17:Unification_dag_exemple.svg n17:Unification_dag_exemple_quadratique.svg dbpedia-fr:Gérard_Huet dbpedia-fr:NC_(complexité) dbpedia-fr:P_(complexité) category-fr:Langage_de_programmation_logique dbpedia-fr:Démonstration_automatique_de_théorèmes dbpedia-fr:Complexité_en_temps dbpedia-fr:Complexité_en_espace dbpedia-fr:Filtrage_par_motif dbpedia-fr:Inférence_de_types dbpedia-fr:Algorithme dbpedia-fr:Programmation_logique category-fr:Syntaxe dbpedia-fr:Prolog dbpedia-fr:Anti-unification dbpedia-fr:Règle_de_résolution dbpedia-fr:Traitement_automatique_des_langues category-fr:Logique_mathématique category-fr:Logique
dbo:wikiPageExternalLink
n25:
dbo:wikiPageLength
43793
dct:subject
category-fr:Algèbre category-fr:Réécriture category-fr:Langage_de_programmation_logique category-fr:Logique category-fr:Logique_mathématique category-fr:Informatique_théorique category-fr:Syntaxe
prop-fr:wikiPageUsesTemplate
n10:= n16:début n10:Section_vide_ou_incomplète n16:fin n10:Quoi n10:Portail n10:Mvar n10:Référence_nécessaire n10:Références n10:, n10:Article_détaillé n10:Souligner n10:Passage_évasif n10:Autres_projets n10:Voir_homonymes
prov:wasDerivedFrom
wikipedia-fr:Unification?oldid=187881412&ns=0
foaf:depiction
n22:John_Alan_Robinson_IMG_0493.jpg n22:Unification_animation.gif n22:Unification_dag_exemple.svg n22:Unification_dag_exemple_quadratique.svg
dbo:thumbnail
n22:Unification_animation.gif?width=300
foaf:isPrimaryTopicOf
wikipedia-fr:Unification
dbo:abstract
En informatique et en logique, l'unification est un processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques. Par exemple, et peuvent être rendus identiques par la substitution et , qui donne quand on l'applique à chacun de ces termes le terme . Dit autrement, l'unification est la résolution d'une équation dans l'algèbre des termes (unification syntaxique) ou dans une algèbre quotient par un ensemble d'identités (unification modulo une théorie) ; la solution de l'équation est la substitution qui rend les deux termes identiques et que l'on appelle l'unificateur.L'unification a des applications en inférence de types, programmation logique, en démonstration automatique de théorèmes, en système de réécriture, en traitement du langage naturel. Souvent, on s'intéresse à l'unification syntaxique où il faut que les termes obtenus par application de l'unificateur soient syntaxiquement égaux, comme dans l'exemple ci-dessus. Par exemple, le problème d'unification syntaxique ayant pour données et n'a pas de solution. Le filtrage par motif (ou pattern matching) est une restriction de l'unification où l'unificateur n'est appliquée qu'à un seul des deux termes. Par exemple, et sont rendus égaux par la substitution . La fin de l'article présente aussi l'unification modulo une théorie, qui est le cas où on dispose de connaissances supplémentaires sur les fonctions (par exemple, est commutatif).