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.

Property Value
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. (cs)
  • 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)
  • 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, that is, a set covering all its solutions, and containing 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)
  • 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)
  • 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)
  • Уніфікація в логіці та інформатиці — це алгоритмічний процес розв'язання рівнянь між символічними . Залежно від того, яким виразам (термам) дозволено з'являтись в наборі рівнянь (також називається проблемою уніфікації), і які вирази вважаються рівними, виділяють кілька структур уніфікації. Якщо у виразі допускаються змінні вищого порядку, тобто змінні, що представляють функції, процес називається уніфікація вищого порядку, інакше, уніфікація першого порядку. Якщо потрібно, щоб обидві сторони кожного рівняння були буквально рівними, цей процес називається синтаксичним або вільним уніфікація, в іншому випадку — семантичне або рівноправна уніфікація, або Е-уніфікація або теорія модулів уніфікації. Рішення проблеми уніфікації позначається як , тобто відображення, що присвоює символічне значення кожній змінній виразів задачі. Алгоритм уніфікації повинен обчислити для заданої задачі повний і мінімальний набір підстановок, тобто набір, що охоплює всі його рішення, і не містить зайвих членів. Залежно від структури, повний та мінімальний набір заміни може мати не більше одного, не більше ніж кінцевого числа або, можливо, нескінченно багато членів або може не існувати зовсім. В деяких рамках взагалі неможливо вирішити, чи існує якесь рішення. Для синтаксичної уніфікації першого порядку Мартеллі та Монтанарі подали алгоритм, який повідомляє про нерозв'язність, або обчислює повний і мінімальний синтаксичний набір, який містить так званий найбільш загальний уніфікатор. Наприклад, використовуючи 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)
  • 本文有关计算机科学主题。其他学科的条目参见合一 (消歧义)。 在数理逻辑中,特别是应用于计算机科学中,两个项的同一是就特殊化次序而言的并(格的最小上界), 就是说,我们在项的集合上假定一个预序,其中 t* ≤ t 意味着 t* 是通过代换(substitute)在 t 中某些项的一个或多个自由变量而从 t 获得的。s 和 t 的同一 u,如果存在的话,是 s 和 t 二者的代换实例的一个项。s 和 t 的任何公共的代换实例也是 u 的实例。 例如,对于多项式 X2 和 Y3 可以通过采纳 X = Z3 和 Y = Z2 而同一到 Z6。 (zh)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 54432 (xsd:integer)
dbo:wikiPageLength
  • 65799 (xsd:integer)
dbo:wikiPageRevisionID
  • 984428808 (xsd:integer)
dbo:wikiPageWikiLink
dbp:quote
  • Symbols are ordered such that variables precede function symbols. Terms are ordered by increasing written length; equally long terms are ordered lexicographically. For a set T of terms, its disagreement path p is the lexicographically least path where two member terms of T differ. Its disagreement set is the set of subterms starting at p, formally: }. Algorithm: Given a set T of terms to be unified Let initially be the identity substitution do forever if is a singleton set then return fi let D be the disagreement set of let s, t be the two lexicographically least terms in D if s is not a variable or s occurs in t then return "NONUNIFIABLE" fi done (en)
dbp:title
  • Robinson's 1965 unification algorithm (en)
dbp:wikiPageUsesTemplate
dct:subject
rdf:type
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. (cs)
  • Если в формулу вместо переменных подставить соответственно формулы то получится формула , которая называется частным случаем формулы : Каждая формула подставляется вместо всех вхождений переменной . Набор подстановок называется унификатором. (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)
  • 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)
  • 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)
  • 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)
rdfs:label
  • Unification (computer science) (en)
  • Unifikace (logika) (cs)
  • Unifikation (Logik) (de)
  • Unification (fr)
  • Unifikacja (informatyka) (pl)
  • Частный случай формулы (ru)
  • Unificação (pt)
  • Уніфікація (інформатика) (uk)
  • 合一 (zh)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:knownFor of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:knownFor of
is foaf:primaryTopic of