| dbo:abstract
|
- 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)
- 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, o E-Unificación o teoría de unificación modular. Una solución de un problema de unificación se denota como una , esto es, un mapeo asignando un valor simbólico a cada una de las variables en las expresiones del problema. Un algoritmo de unificación debe calcular un conjunto de sustituciones completo y mínimo para un problema dado; esto es, un conjunto que cubra todas las soluciones y que no contenga miembros redundantes. De acuerdo con el marco de referencia, un conjunto de sustituciones completo y mínimo puede que tenga a lo más un miembro, a lo sumo una cantidad finita, o posiblemente infinito número de miembros, o no tener ninguno del todo. En algunos marcos de referencia es generalmente imposible decidir siquiera si existe alguna solución. Para unificaciones sintácticas de primer orden, Martelli y Montanari brindaron un algoritmo que reporta insolubilidd o calcula un conjunto completo y mínimo de sustituciones unitario que contiene el así llamado unificador más general. Por ejemplo, usando x,y,z como variables, el conjunto de ecuaciones unitario { (x,cons(x,)) = cons(2,y) } es un problema de unificación sintáctico de primer orden que tiene la sustitución { x ↦ 2, y ↦ cons(2,nil) } como única solución. El problema de unificación sintáctico de primer orden { y = cons(2,y) } no tiene solución en el conjunto ; sin embargo, tiene una solución única { y ↦ cons(2,cons(2,cons(2,...))) } en el conjunto de . El problema de unificación semántica de primer orden { a⋅x = x⋅a } tiene cualquier sustitución de la forma { x ↦ a⋅...⋅a } como solución en un semigrupo, en otras palabras, si (⋅) es asociativa; el mismo problema, visto en un grupo abeliano donde (⋅) también es considerada conmutativa, tiene cualquier sustitución como una solución. El conjunto unitario { a = y(x) } es un problema de unificación sintáctico de segundo orden dado que y es una variable que representa una función. Una solución es { x ↦ a, y ↦ (función identidad) }; otra solución es { y ↦ (función constante asociando cada valor con a), x ↦ (cualquier valor) }. Los algoritmos de unificación fueron descubiertos por Jacques Herbrand, pero la primera investigación formal puede ser atribuida a , quien utilizó unificación sintáctica de primer orden como base en su procedimiento de resolución de lógica de primer orden, un gran paso adelante en la tecnología de razonamiento automatizado al eliminar una de las fuentes de explosión combinatoria: la búsqueda de instanciación de términos. El razonamiento automático es todavía el área donde la unificación es aplicada mayormente. Unificación sintáctica de primer orden es usada en programación lógica y en la implementación de lenguajes de programación que usan , especialmente en algoritmos de inferencia de tipos basados en . Unificación semántica es utilizada en solucionadores de satisfacibilidad módulo (SMT por las siglas en inglés), algoritmos para la (reescritura de términos) y en análisis de protocolos criptográficos. Unificación de orden superior es utilizado en asistentes para la demostración de teoremas, por ejemplo Isabelle and , y formas restringidas de unificación de orden superior (unificación de patrones de nivel orden superior) son utilizadas en la implementación de algunos lenguajes de programación, tales como , porque pese a que los patrones de orden superior son expresivos, su procedimiento de unificación asociado conserva propiedades teóricas más cercanas a la unificación de primer orden. (es)
- 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. Als Basisoperation liegt der Unifikation die Substitution zu Grunde. Im Rahmen der Prädikatenlogik bedeutet eine Substitution σ innerhalb eines gegebenen Ausdrucks die Ersetzung einer Variablen durch einen Term, in dem diese Variable nicht vorkommen darf. Die Variable wird gewissermaßen durch den Term „instanziiert“. Wird eine Menge von Ausdrücken durch eine Substitution σ zu einem äquivalenten Ausdruck substituiert, d. h. , so bezeichnet man σ als Unifikator dieser Ausdrucksmenge. Die Anwendung eines Unifikators auf diese Menge bezeichnet man als Unifikation. Nicht alle Ausdrucksmengen können unifiziert werden. (de)
- 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). (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. A solution of a unification problem is denoted as a substitution, that is, a mapping assigning a symbolic value to each variable of the problem's expressions. A unification algorithm should compute for a given problem a complete and minimal substitution set, i.e., a set containing all of the problem's solutions and no redundant members. Depending on the framework, a complete and minimal substitution set may have at most one, at most finitely many, or possibly infinitely many members, or may not exist at all. In some frameworks it is generally impossible to decide whether any solution exists. For first-order syntactical unification, Martelli and Montanari gave an algorithm that reports unsolvability or computes a complete and minimal singleton substitution set containing the so-called most general unifier. For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution.The syntactic first-order unification problem { y = cons(2,y) } has no solution over the set of finite terms; however, it has the single solution { y ↦ cons(2,cons(2,cons(2,...))) } over the set of infinite trees.The semantic first-order unification problem { a⋅x = x⋅a } has each substitution of the form { x ↦ a⋅...⋅a } as a solution in a semigroup, i.e. if (⋅) is considered associative; the same problem, viewed in an abelian group, where (⋅) is considered also commutative, has any substitution at all as a solution.The singleton set { a = y(x) } is a syntactic second-order unification problem, since y is a function variable.One solution is { x ↦ a, y ↦ (identity function) }; another one is { y ↦ (constant function mapping each value to a), x ↦ (any value) }. A unification algorithm was first discovered by Jacques Herbrand, while a first formal investigation can be attributed to John Alan Robinson, who used first-order syntactical unification as a basic building block of his resolution procedure for first-order logic, a great step forward in automated reasoning technology, as it eliminated one source of combinatorial explosion: searching for instantiation of terms. Today, automated reasoning is still the main application area of unification.Syntactical first-order unification is used in logic programming and programming language type system implementation, especially in Hindley–Milner based type inference algorithms.Semantic unification is used in SMT solvers, term rewriting algorithms and cryptographic protocol analysis.Higher-order unification is used in proof assistants, for example Isabelle and Twelf, and restricted forms of higher-order unification (higher-order pattern unification) are used in some programming language implementations, such as lambdaProlog, as higher-order patterns are expressive, yet their associated unification procedure retains theoretical properties closer to first-order unification. (en)
- ユニフィケーション（英: unification）は数理論理学や計算機科学の用語であり、問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つのが同一または同等であることを示すを求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。 なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。 主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が同一であることを示すためのユニフィケーションは統語論的ユニフィケーションと呼ばれる。空でない等号を持つ論理（理論）で2つの項の同等性を示す場合、それを意味論的ユニフィケーションと呼ぶ。置換は順序集合として順序付けられるので、ユニフィケーションは束における結びを求める手続きとして解釈できる。 ユニフィケーションアルゴリズムはジャック・エルブランによって最初に発見されたが、ユニフィケーションを初めて形式的に研究したのはで、一階述語論理の導出手続きを構築する際に一階のユニフィケーションを基盤として使い、組合せ爆発の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。 (ja)
- 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:
* jeśli po jednej stronie jest zmienna, dorzucamy ją do unifikatora i zamieniamy wszystkie jej wystąpienia na to co występuje po drugiej stronie. Należy zająć się też przypadkiem szczególnym, kiedy druga strona zawiera wystąpienie tej zmiennej – zależnie od implementacji x i (+ x 1) mogą się unifikować, nie unifikować, bądź też powodować niezamierzone zapętlenie.
* jeśli po obu stronach są te same stałe, unifikacja się powiodła
* jeśli po obu stronach są te same relacje n-arne, unifikacja się powiodła o ile powiodła się unifikacja wszystkich n-poddrzew, przy czym unifikator dotyczy wszystkich poddrzew.
* jeśli po obu stronach są różne stałe bądź relacje, unifikacja się nie powiodła. (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 equacional, ou unificação E, ou unificação módulo uma teoria. A solução de um problema de unificação é denotada como uma , isto é, um mapeamento atribuindo um valor simbólico a cada variável das expressões do problema. Um algoritmo de unificação deve computar, para um dado problema, um conjunto de substituição completo e mínimo, isto é, um conjunto cobrindo todas as soluções e com nenhum membro redundante. Dependendo da estrutura, um conjunto de substituição completo e mínimo talvez contenha nenhum, ou uma quantidade finita, ou infinita de membros. [nota1] Em algumas estruturas é geralmente impossível decidir se existe alguma solução. Para a unificação sintática de primeira ordem, Martelli e Montanari desenvolveram um algoritmo capaz de informar a inexistência de uma solução ou computar um único conjunto de substituição completo e mínimo contendo o chamado unificador mais geral. Por exemplo, usando x, y, z como variáveis e o único conjunto de equação { (x,cons(x,nil)) = cons(2,y) } é um problema unificação sintática de primeira ordem que tem a substituição { x ↦ 2, y ↦ cons(2,nil) } como uma única solução. O problema da unificação sintática de primeira ordem { y = cons(2,y) } não possui uma solução sobre o conjunto de termos finitos; contudo, possui como solução única { y ↦ cons(2,cons(2,cons(2,...))) } sobre o conjunto de árvores infinitas. O problema da unificação semântica de primeira ordem { a⋅x = x⋅a } possui toda substituição da forma { x ↦ a⋅...⋅a } como uma solução em um semi grupo, isto é, se (⋅) é considerado associativo; o mesmo problema, visto em um grupo abeliano, onde (⋅) é considerado também como comutativo, tem qualquer substituição como uma solução. O único conjunto { a = y(x) } é um problema se unificação sintático de segunda ordem, desde que y seja uma função variável. Uma solução é { x ↦ a, y ↦ (função identidade) }; outra solução é { y ↦ ( mapeando cada valor para a), x ↦ (qualquer valor) }. A primeira investigação formal de unificação pode ser atribuída a , quem usou a unificação sintática de primeira ordem como um bloco básico de construção em seu processo de resolução para a lógica de primeira ordem, um bom avanço na tecnologia de , uma vez que isso eliminou uma fonte de explosão combinatória: busca por instanciação de termos. Hoje, o raciocínio automatizado continua sendo a principal área de aplicação da unificação. A unificação sintática de primeira ordem é usada na lógica de programação e na implementação de sistema de tipos na linguagem de programação, especialmente nos tipos de algoritmos de inferência baseados em . A unificação semântica é usada em e em algoritmos de reescrita de termos. Unificação de alta ordem é usada em assistentes de provas, por exemplo, Isabelle e , e formas restritas da unificação de alta ordem (padrão de unificação de alta ordem) são usadas em algumas implementações de linguagens de programação, no caso de lambdaProlog. Como padrões de alta ordem são expressivos, seu processo de unificação associada ainda retêm propriedades teóricas próximas a unificação de primeira ordem. (pt)
- Если в формулу вместо переменных подставить соответственно формулы то получится формула , которая называется частным случаем формулы : Каждая формула подставляется вместо всех вхождений переменной . Набор подстановок называется унификатором. (ru)
- 在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并(格的最小上界), 就是说，我们在项的集合上假定一个预序，其中 t* ≤ t 意味着 t* 是通过代换(substitute)在 t 中某些项的一个或多个自由变量而从 t 获得的。s 和 t 的同一 u，如果存在的话，是 s 和 t 二者的代换实例的一个项。s 和 t 的任何公共的代换实例也是 u 的实例。 例如，对于多项式 X2 和 Y3 可以通过采纳 X = Z3 和 Y = Z2 而同一到 Z6。 (zh)
- Уніфікація в логіці та інформатиці — це алгоритмічний процес розв'язання рівнянь між символічними . Залежно від того, яким виразам (термам) дозволено з'являтись в наборі рівнянь (також називається проблемою уніфікації), і які вирази вважаються рівними, виділяють кілька структур уніфікації. Якщо у виразі допускаються змінні вищого порядку, тобто змінні, що представляють функції, процес називається уніфікація вищого порядку, інакше, уніфікація першого порядку. Якщо потрібно, щоб обидві сторони кожного рівняння були буквально рівними, цей процес називається синтаксичним або вільним уніфікація, в іншому випадку — семантичне або рівноправна уніфікація, або Е-уніфікація або теорія модулів уніфікації. Рішення проблеми уніфікації позначається як , тобто відображення, що присвоює символічне значення кожній змінній виразів задачі. Алгоритм уніфікації повинен обчислити для заданої задачі повний і мінімальний набір підстановок, тобто набір, що охоплює всі його рішення, і не містить зайвих членів. Залежно від структури, повний та мінімальний набір заміни може мати не більше одного, не більше ніж кінцевого числа або, можливо, нескінченно багато членів або може не існувати зовсім. В деяких рамках взагалі неможливо вирішити, чи існує якесь рішення. Для синтаксичної уніфікації першого порядку Мартеллі та Монтанарі подали алгоритм, який повідомляє про нерозв'язність, або обчислює повний і мінімальний синтаксичний набір, який містить так званий найбільш загальний уніфікатор. Наприклад, використовуючи x,y,z як змінні, встановлюється рівняння: { cons(x,cons(x, nil)) = cons (2, y) } — це синтаксична проблема уніфікації першого порядку що має єдине рішення для заміни { x ↦ 2, y ↦ cons(2, nil)}. Синтаксична проблема уніфікації першого порядку ( y = cons (2, y)} не має вирішення над набором кінцевих виразів; однак у нього є єдине рішення { y ⟩ cons (2, cons (2, cons (2, …)))} над набором нескінченних дерев. Семантична проблема уніфікації першого порядку {a⋅x = x⋅a} має кожну підстановку форми { x ↦ "'a' ' ⋅ … ⋅a } як рішення в напівгрупи, тобто якщо (⋅) вважається асоціативна; та ж проблема, розглянута в абелевій групі, де (⋅) також вважається комутативна, має взагалі будь-яку заміну як рішення.Синтаксична задача уніфікації другого порядку, оскільки y — функціональна змінна, є синтаксичною задачею { a = y ( x ) }.Одним із рішень є {x ↦ a, y ↦ (тотожність функції)}; інший є {y ↦ (стала функція, що відслідковує кожне значення до a), x ↦ (будь-яке значення)}. Перше формальне дослідження уніфікації можна віднести до Джон Алан Робінсон,, який застосував синтаксичне уніфікація першого порядку як базовий будівельний блок його рішення процедури логіки першого порядку, великий крок вперед в автоматизоване обґрунтування технології, оскільки вона усуває одне джерело комбінаторного вибуху: пошук об'єктів термінів. Сьогодні автоматизовані міркування залишаються головною областю застосування уніфікації. Синтаксичне уніфікація першого порядку використовується для здійснення логічного програмування та реалізації мови програмування типа даних, особливо в на основі алгоритму виведення типу.Семантичне об'єднання використовується в алгоритмах Satisfiability Modulo Theories, алгоритмах рерайтинг та аналізі криптографічного протоколу.Об'єднання більш високого порядку використовується в асистентах-доказах, наприклад , а також обмежені форми уніфікації більш високого порядку (уніфікація шаблонів вищого порядку) використовуються в деяких реалізаціях мов програмування, таких як , оскільки шаблони вищих порядків є експресивними, проте їх пов'язана процедура уніфікації зберігає теоретичні властивості ближче до уніфікації першого порядку. (uk)
|
| 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)
|
