| dbo:abstract
|
- Anti-unification is the process of constructing a generalization common to two given symbolic expressions. As in unification, several frameworks are distinguished depending on which expressions (also called terms) are allowed, and which expressions are considered equal. If variables representing functions are allowed in an expression, the process is called "higher-order anti-unification", otherwise "first-order anti-unification". If the generalization is required to have an instance literally equal to each input expression, the process is called "syntactical anti-unification", otherwise "E-anti-unification", or "anti-unification modulo theory". An anti-unification algorithm should compute for given expressions a complete, and minimal generalization set, that is, a set covering all generalizations, and containing no redundant members, respectively. Depending on the framework, a complete and minimal generalization set may have one, finitely many, or possibly infinitely many members, or may not exist at all; it cannot be empty, since a trivial generalization exists in any case. For first-order syntactical anti-unification, Gordon Plotkin gave an algorithm that computes a complete and minimal singleton generalization set containing the so-called "least general generalization" (lgg). Anti-unification should not be confused with dis-unification. The latter means the process of solving systems of inequations, that is of finding values for the variables such that all given inequations are satisfied. This task is quite different from finding generalizations. (en)
- El anti-unificación es el proceso de construir una generalización común a dos expresiones simbólicas dadas. Al igual que en la unificación, se distinguen varios marcos de trabajo dependiendo de qué expresiones (también llamadas términos) están permitidas y qué expresiones se consideran iguales. Si las variables que representan funciones están permitidas en una expresión, el proceso se llama "anti-unificación de orden superior", de lo contrario se lo llama "anti-unificación de primer orden". Si se requiere que la generalización tenga una instancia literalmente igual a cada expresión de entrada, el proceso se llama "anti-unificación sintáctica", de lo contrario "E-anti-unificación" o "teoría del módulo de anti-unificación". Un algoritmo de anti-unificación debería calcular para las expresiones dadas un conjunto de generalización completo y mínimo, es decir, un conjunto que cubra todas las generalizaciones y que no contenga miembros redundantes, respectivamente. Dependiendo del marco de trabajo, un conjunto de generalización completo y mínimo puede tener uno, muchos, posiblemente infinitos miembros, o puede no existir en absoluto; no puede estar vacío, ya que existe una generalización trivial en cualquier caso. Para la anti-unificación sintáctica de primer orden, proporcionó un algoritmo que calcula un conjunto de generalización singleton completo y mínimo que contiene la llamada "generalización menos general" (least general generalization, LGG). La anti-unificación no debe confundirse con la . Esto último significa el proceso de resolver sistemas de inecuaciones, es decir, encontrar valores para las variables de modo que se satisfagan todas las inecuaciones dadas. Esta tarea es bastante diferente de encontrar generalizaciones. (es)
- En informatique théorique et en logique mathématique, l'anti-unification est la construction d'une généralisation commune à deux termes symboliques données. Comme son nom l’indique, c'est l'opération duale[évasif] de l'unification qui est le calcul de l'instance la plus générale des termes. Des problèmes d'anti-unification se posent dans de nombreuses branches de l'intelligence artificielle : apprentissage machine, raisonnement analogique et basé sur des cas, modélisation cognitive, découverte de connaissances, etc. L'anti-unification est une technique souvent utilisée pour résoudre les problèmes de généralisation. Comme pour l’unification, on distingue plusieurs niveaux selon la nature des termes considérés du premier ordre ou d'ordre supérieur, termes nominaux, arbres, et autres. (fr)
- 反ユニフィケーションとは、2つの与えられた記号式に共通の一般化を構築するプロセスである。ユニフィケーションと同様に、許可される式(用語とも呼ばれる)と、等しいと見なされる式に応じて分類できる。関数を表す変数が式で許可されている場合、そのプロセスは「高階反ユニフィケーション」と呼ばれ、そうでない場合は「一次反ユニフィケーション」と呼ばれる。一般化が各入力式に文字通り等しいインスタンスを持つ必要がある場合、プロセスは「構文的反ユニフィケーション」や「E-反ユニフィケーション」または「反ユニフィケーションモジュロ理論」と呼ばれる。 (ja)
- Antiunificação é o processo de construção de uma generalização comum a duas expressões simbólicas. Como na unificação, várias estruturas são distinguidas dependendo de qual das expressões (também denominado termos) são permitidas e quais expressões são consideradas iguais. Se as variáveis que representam funções são permitidas em uma expressão, o processo é chamado de antiunificação de ordem superior, caso contrário, de antiunificação de primeira ordem. Se a generalização requer a existência de uma instância literalmente igual para cada expressão de entrada, o processo é chamado de antiunificação sintática, caso contrário, de E-antiunificação, ou módulo da teoria da antiunificação. Um algoritmo de antiunificação deve calcular, para expressões dadas, uma generalização completa e mínima de um conjunto, isto é, um conjunto, abrangendo todas as generalizações, e que não contenha membros redundantes, respectivamente. Dependendo da estrutura, uma generalização completa e mínima pode ter um, finitamente muitos, ou, possivelmente, um número infinito de membros, ou pode não existir; ela não pode ser vazia, uma vez que uma generalização trivial existe em qualquer caso. Para a antiunificação de primeira-ordem sintática, Gordon Plotkin apresentou um algoritmo que calcula uma generalização completa e mínima de um conjunto unitário, o chamado menor generalização geral (mgg). Antiunificação não deve ser confundido com o . O segundo significa o processo de resolução de sistemas deinequações, que é de encontrar valores para as variáveis de tal forma que todas as inequações sejam satisfeitas. Esta tarefa é bastante diferente da busca de generalizações. (pt)
|
| rdfs:comment
|
- 反ユニフィケーションとは、2つの与えられた記号式に共通の一般化を構築するプロセスである。ユニフィケーションと同様に、許可される式(用語とも呼ばれる)と、等しいと見なされる式に応じて分類できる。関数を表す変数が式で許可されている場合、そのプロセスは「高階反ユニフィケーション」と呼ばれ、そうでない場合は「一次反ユニフィケーション」と呼ばれる。一般化が各入力式に文字通り等しいインスタンスを持つ必要がある場合、プロセスは「構文的反ユニフィケーション」や「E-反ユニフィケーション」または「反ユニフィケーションモジュロ理論」と呼ばれる。 (ja)
- Anti-unification is the process of constructing a generalization common to two given symbolic expressions. As in unification, several frameworks are distinguished depending on which expressions (also called terms) are allowed, and which expressions are considered equal. If variables representing functions are allowed in an expression, the process is called "higher-order anti-unification", otherwise "first-order anti-unification". If the generalization is required to have an instance literally equal to each input expression, the process is called "syntactical anti-unification", otherwise "E-anti-unification", or "anti-unification modulo theory". (en)
- El anti-unificación es el proceso de construir una generalización común a dos expresiones simbólicas dadas. Al igual que en la unificación, se distinguen varios marcos de trabajo dependiendo de qué expresiones (también llamadas términos) están permitidas y qué expresiones se consideran iguales. Si las variables que representan funciones están permitidas en una expresión, el proceso se llama "anti-unificación de orden superior", de lo contrario se lo llama "anti-unificación de primer orden". Si se requiere que la generalización tenga una instancia literalmente igual a cada expresión de entrada, el proceso se llama "anti-unificación sintáctica", de lo contrario "E-anti-unificación" o "teoría del módulo de anti-unificación". (es)
- En informatique théorique et en logique mathématique, l'anti-unification est la construction d'une généralisation commune à deux termes symboliques données. Comme son nom l’indique, c'est l'opération duale[évasif] de l'unification qui est le calcul de l'instance la plus générale des termes. (fr)
- Antiunificação é o processo de construção de uma generalização comum a duas expressões simbólicas. Como na unificação, várias estruturas são distinguidas dependendo de qual das expressões (também denominado termos) são permitidas e quais expressões são consideradas iguais. Se as variáveis que representam funções são permitidas em uma expressão, o processo é chamado de antiunificação de ordem superior, caso contrário, de antiunificação de primeira ordem. Se a generalização requer a existência de uma instância literalmente igual para cada expressão de entrada, o processo é chamado de antiunificação sintática, caso contrário, de E-antiunificação, ou módulo da teoria da antiunificação. (pt)
|
