| rdfs:comment
| - Unifikace je v logice , po jejíž aplikaci na množinu termů dostaneme jeden term. Formálně, je-li a t a s dva termy, je substituce jejich unifikací, pokud .Algoritmus unifikace termů predikátové logiky byl poprvé formulován Alanem Robinsonem v roce 1965 a použit pro rezoluci v predikátové logice. Používá se například v unifikačních gramatikách. (cs)
- ユニフィケーション（英: unification）は数理論理学や計算機科学の用語であり、問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つのが同一または同等であることを示すを求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。 なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。 主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が同一であることを示すためのユニフィケーションは統語論的ユニフィケーションと呼ばれる。空でない等号を持つ論理（理論）で2つの項の同等性を示す場合、それを意味論的ユニフィケーションと呼ぶ。置換は順序集合として順序付けられるので、ユニフィケーションは束における結びを求める手続きとして解釈できる。 ユニフィケーションアルゴリズムはジャック・エルブランによって最初に発見されたが、ユニフィケーションを初めて形式的に研究したのはで、一階述語論理の導出手続きを構築する際に一階のユニフィケーションを基盤として使い、組合せ爆発の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。 (ja)
- Если в формулу вместо переменных подставить соответственно формулы то получится формула , которая называется частным случаем формулы : Каждая формула подставляется вместо всех вхождений переменной . Набор подстановок называется унификатором. (ru)
- 在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并(格的最小上界), 就是说，我们在项的集合上假定一个预序，其中 t* ≤ t 意味着 t* 是通过代换(substitute)在 t 中某些项的一个或多个自由变量而从 t 获得的。s 和 t 的同一 u，如果存在的话，是 s 和 t 二者的代换实例的一个项。s 和 t 的任何公共的代换实例也是 u 的实例。 例如，对于多项式 X2 和 Y3 可以通过采纳 X = Z3 和 Y = Z2 而同一到 Z6。 (zh)
- Unifikation ist eine Methode zur Vereinheitlichung prädikatenlogischer Ausdrücke. Zwei Ausdrücke werden unifiziert, indem ihre Variablen so durch geeignete Terme ersetzt werden, dass die resultierenden Ausdrücke gleich sind. Die Unifikation hat insbesondere in der Computerlogik und Computerlinguistik eine größere Bedeutung erlangt. So nutzt etwa die Inferenzmaschine des Prolog-Interpreters Unifikation. In der Computerlinguistik gibt es sogenannte Unifikationsgrammatiken, die sich auf dieses Konzept stützen. Auch beim Theorembeweisen spielt Unifikation eine große Rolle. (de)
- En lógica y en ciencias de la computación, la unificación es un proceso algorítmico para resolución de ecuaciones con expresiones simbólicas. Se pueden determinar diferentes esquemas de unificación dependiendo de: qué expresiones (también llamadas términos) están permitidas en un conjunto de ecuaciones (también llamado problema de unificación), y de cuáles expresiones son consideradas homólogas. Si variables de orden superior, esto es, variables que representan funciones, son permitidas en una expresión, el proceso es llamado unificación de orden superior, si no se llama unificación de primer orden. Si una solución requiere hacer ambos lados de cada ecuación literalmente iguales entonces el proceso se llama sintáctico o unificación libre, de lo contrario semántico o unificación ecuacional, (es)
- 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 (fr)
- In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions. Depending on which expressions (also called terms) are allowed to occur in an equation set (also called unification problem), and which expressions are considered equal, several frameworks of unification are distinguished. If higher-order variables, that is, variables representing functions, are allowed in an expression, the process is called higher-order unification, otherwise first-order unification. If a solution is required to make both sides of each equation literally equal, the process is called syntactic or free unification, otherwise semantic or equational unification, or E-unification, or unification modulo theory. (en)
- Unifikacja (ang. unification) – operacja na dwóch lub więcej drzewach, która znajduje takie przyporządkowanie zmiennych, że drzewa te są równe. Np. (w notacji lispowej): (+ x 2) i (+ (+ z 7) y) są unifikowalne dla y=2 i x=(+ z 7). (+ x 2) i (+ y 3) nie są unifikowalne. Podobnie unifikowalne nie są (* x 2) i (+ x x) ani (+ 2 3) i (+ 3 2) – unifikacja dotyczy tylko symboli, a nie ich znaczenia. Unifikator to wygenerowany w ten sposób zbiór przyporządkowań. Algorytm wygląda tak: (pl)
- Unificação, em ciência da computação e na lógica, é um processo algorítmico de solução de equações entre expressões simbólicas. Dependendo de quais expressões (também chamadas de termos) são permitidas ocorrer em um conjunto de equações (também chamado de problema da unificação), e quais expressões são consideradas iguais, diversas estruturas de unificação são distinguidas. Se variáveis de alta ordem, isto é, variáveis que representam funções, são permitidas em uma expressão, o processo é chamado de unificação de alta ordem, ou, caso contrário, é chamado de unificação de primeira ordem. Se exige-se uma solução que faça com que ambos os lados de cada equação sejam literalmente iguais, o processo é chamado de unificação sintática, ou, caso contrário, unificação semântica, ou unificação equac (pt)
- Уніфікація в логіці та інформатиці — це алгоритмічний процес розв'язання рівнянь між символічними . Залежно від того, яким виразам (термам) дозволено з'являтись в наборі рівнянь (також називається проблемою уніфікації), і які вирази вважаються рівними, виділяють кілька структур уніфікації. Якщо у виразі допускаються змінні вищого порядку, тобто змінні, що представляють функції, процес називається уніфікація вищого порядку, інакше, уніфікація першого порядку. Якщо потрібно, щоб обидві сторони кожного рівняння були буквально рівними, цей процес називається синтаксичним або вільним уніфікація, в іншому випадку — семантичне або рівноправна уніфікація, або Е-уніфікація або теорія модулів уніфікації. (uk)
|
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)
![[RDF Data]](/fct/images/sw-rdf-blue.png)