| dbpprop:abstract
|
- In mathematical logic, in particular as applied to computer science, a unification of two terms is a join (in the lattice sense) with respect to a specialisation order. That is, we suppose a preorder on a set of terms, for which t* ≤ t means that t* is obtained from t by substituting some term(s) for one or more free variables in t. The unification u of s and t, if it exists, is a term that is a substitution instance of both s and t. If any common substitution instance of s and t is also an instance of u, u is called minimal unification. For example, with polynomials, X and Y can be unified to Z by taking X = Z and Y = Z.
- Unifikation ist eine Methode zur Vereinheitlichung prädikatenlogischer Ausdrücke. Diese 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 <math>\{A_1,A_2,... ,A_n \}</math> durch eine Substitution σ zu einem äquivalenten Ausdruck substituiert, d. h. <math> \sigma(A_1) \equiv \sigma(A_2) \equiv ... \equiv \sigma(A_n)</math>, so bezeichnet man σ als Unifikator dieser Ausdrucksmenge. Die Anwendung eines Unifikators auf diese Menge bezeichnet man als Unifikation. Nicht alle Ausdrücke können unifiziert werden!
- Le concept d'unification est une notion centrale de la logique des prédicats ainsi que d'autres systèmes de logique et est sans doute ce qui distingue le plus Prolog des autres langages de programmation. L'unification de deux termes <math>t_1</math> et <math>t_2</math> consiste à trouver (quand il en existe) un troisième terme <math>t</math> tel qu'on puisse passer de <math>t</math> à <math>t_1</math> et à <math>t_2</math> en instanciant certaines variables. <math>t</math> est alors appelé un unificateur de <math>t_1</math> et <math>t_2</math>. Intuitivement, l'unification est le fait d'attribuer une valeur à certaines variables de <math>t_1</math> et <math>t_2</math> et peut être regardé comme un genre d'assignation qui ne pourrait s'effectuer qu'une seule fois. Lorsqu'on résout une équation algébrique, une inconnue peut avoir une, plusieurs ou aucune solutions, mais sa valeur ne change pas durant les opérations; c'est pareil pour l'unification. En fait on peut voir la résolution d'une équation comme un cas particulier d'unification. En prolog, cette opération est dénotée par symbole « = ». Les règles de l'unification sont les suivantes: une variable X non-instanciée (c'est-à-dire ne possédant pas encore de valeur) peut être unifiée avec une autre variable (instanciée ou pas); les deux variables deviennent alors simplement des synonymes l'une de l'autre et représenteront dorénavant la même chose; une variable X non-instanciée peut être unifiée avec un terme ou un atome et représentera dorénavant ce terme ou atome; un atome peut être unifié seulement avec le même atome; un terme peut être unifié avec un autre terme : si leurs noms sont identiques, si leur nombres d'arguments sont identiques et si chacun des arguments du premier terme est unifiable avec l'argument correspondant du second terme. En raison de sa nature déclarative, l'ordre dans une suite d'unifications ne joue (habituellement) aucun rôle.
- ユニフィケーション（Unification）は数理論理学や計算機科学の用語であり、特殊化順序（specialisation order）に従って（束論的意味で）2つの項の結び(join)を求めることである。すなわち、項の集合に t* ≤ t という順序を導入する。ここで、t* は t 内の1つまたは複数の自由変項を項に置換することで得られる項である。s と t のユニフィケーション u は（もしあれば）、s および t の置換実体（substitution instance）となる項である。s と t に共通する置換実体が u の実体でもある場合、u を最小ユニフィケーション（minimal unification）と呼ぶ。 なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。 例えば、多項式 X と Y に関して、X = Z かつ Y = Z であれば、どちらも Z に統一される。
- Innen matematisk logikk, spesielt anvendt innen informatikk, er en unifikasjon av to termer en sammenslåing (av typen en finner for delvis ordnede set) med hensyn til en spesialiserings orden. Det vil si, vi antar en preorden på et sett av termer, der t* ≤ t betyr at t* er utledet fra t ved å substituere en eller flere termer for en eller flere frie variabler i t. Unifikasjonen av u for s og t, om den eksisterer, er en term som er en substitusjons instans av både s og t. Om en felles substitusjons instans for s og t også er en instans for u, u så kalles den for en minimal unifikasjon. For eksempel, kan polynomene, X og Y unifiseres til Z ved å gjøre substitusjonene X = Z og Y = Z. ==Definisjon av unifikasjon for første ordens logikk
- Unifikacja to operacja na dwóch lub więcej drzewach, która znajduje takie przyporządkowanie zmiennych, że drzewa te są równe. Np. : (+ x 2) i (+ 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 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.
- Uma substituição σ é um conjunto de componentes de substituições independentes: σ = [(t1, v1), . . . , (tn, vn)]. O primeiro elemento de cada componente é um termo e o segundo elemento é uma variável, tal que: 1. vi ≠ vj se i ≠ j 2. vi não ocorre em tj para quaisquer i e j. Se uma variável v é trocada em cada uma de suas ocorrências livres, na fbf α, pelo termo t, a fórmula resultante é chamada uma instância de substituição de α, e denotada por α[(t, v)], cuja leitura é “α com t no lugar de v”. Analogamente, α[(t1, v1), . . . , (tn, vn)] denota o resultado de trocar simultaneamente todas as ocorrências das diferentes variáveis v1, . . . , vn, em α, por t1, . . . , tn, respectivamente. Como exemplo, os polinômios, X e Y podem ser unificados a Z tomando σ = [(Z, X), (Z, Y)].
- 在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并, 就是说，我们在项的集合上假定一个预序，其中 t* ≤ t 意味着 t* 是通过代换(substitute)在 t 中某些项的一个或多个自由变量而从 t 获得的。s 和 t 的同一 u，如果存在的话，是 s 和 t 二者的代换实例的一个项。s 和 t 的任何公共的代换实例也是 u 的实例。 例如，对于多项式 X 和 Y 可以通过采纳 X = Z 和 Y = Z 而同一到 Z。
|
| rdfs:comment
|
- In mathematical logic, in particular as applied to computer science, a unification of two terms is a join (in the lattice sense) with respect to a specialisation order. That is, we suppose a preorder on a set of terms, for which t* ≤ t means that t* is obtained from t by substituting some term(s) for one or more free variables in t. The unification u of s and t, if it exists, is a term that is a substitution instance of both s and t.
- Unifikation ist eine Methode zur Vereinheitlichung prädikatenlogischer Ausdrücke. Diese 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.
- Le concept d'unification est une notion centrale de la logique des prédicats ainsi que d'autres systèmes de logique et est sans doute ce qui distingue le plus Prolog des autres langages de programmation.
- Innen matematisk logikk, spesielt anvendt innen informatikk, er en unifikasjon av to termer en sammenslåing (av typen en finner for delvis ordnede set) med hensyn til en spesialiserings orden. Det vil si, vi antar en preorden på et sett av termer, der t* ≤ t betyr at t* er utledet fra t ved å substituere en eller flere termer for en eller flere frie variabler i t. Unifikasjonen av u for s og t, om den eksisterer, er en term som er en substitusjons instans av både s og t.
- Unifikacja to operacja na dwóch lub więcej drzewach, która znajduje takie przyporządkowanie zmiennych, że drzewa te są równe. Np. : (+ x 2) i (+ 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 nie ich znaczenia. Unifikator to wygenerowany w ten sposób zbiór przyporządkowań.
- Uma substituição σ é um conjunto de componentes de substituições independentes: σ = [(t1, v1), . . . , (tn, vn)]. O primeiro elemento de cada componente é um termo e o segundo elemento é uma variável, tal que: 1. vi ≠ vj se i ≠ j 2. vi não ocorre em tj para quaisquer i e j.
|
![[RDF Data]](/statics/sw-cube.png)
