Una red de subsunción es una estructura matemática utilizada en el contexto teórico de la demostración automatizada de teoremas y otras aplicaciones de cálculo simbólico .
Se dice que un término t 1 subsume un término t 2 si existe una sustitución σ tal que σ aplicada a t 1 da como resultado t 2 . En este caso, t 1 también se denomina más general que t 2 , y t 2 se denomina más específico que t 1 , o una instancia de t 1 .
El conjunto de todos los términos (de primer orden) sobre una firma dada se puede convertir en una red sobre la relación de ordenamiento parcial " ... es más específico que... " de la siguiente manera:
Esta red se denomina red de subsunción. Se dice que dos términos son unificables si su punto de encuentro es distinto de Ω.
Las operaciones de unión y encuentro en esta red se denominan antiunificación y unificación , respectivamente. Una variable x y el elemento artificial Ω son el elemento superior e inferior de la red, respectivamente. Cada término fundamental , es decir, cada término sin variables, es un átomo de la red. La red tiene infinitas cadenas descendentes , por ejemplo , x , g ( x ), g ( g ( x )), g ( g ( g ( x ))), ..., pero no infinitas ascendentes.
Si f es un símbolo de función binaria, g es un símbolo de función unaria, y x e y denotan variables, entonces los términos f ( x , y ), f ( g ( x ), y ), f ( g ( x ), g ( y )), f ( x , x ), y f ( g ( x ), g ( x )) forman la red mínima no modular N 5 (véase la figura 1); su apariencia impide que la red de subsunción sea modular y, por lo tanto, también distributiva .
El conjunto de términos unificables con un término dado no necesita ser cerrado respecto de su cumplimiento; la figura 2 muestra un contraejemplo.
Denotando por Gnd( t ) el conjunto de todas las instancias fundamentales de un término t , se cumplen las siguientes propiedades: [2]
El conjunto de términos lineales , es decir, de términos sin ocurrencias múltiples de una variable, es un subconjunto de la red de subsunción y es en sí misma una red. Esta red también incluye N 5 y la red mínima no distributiva M 3 como subredes (ver Figuras 3 y 4) y, por lo tanto, no es modular, y mucho menos distributiva.
La operación de encuentro siempre produce el mismo resultado en la red de todos los términos que en la red de términos lineales. La operación de unión en la red de todos los términos produce siempre una instancia de la unión en la red de términos lineales; por ejemplo, los términos (fundamentales) f ( a , a ) y f ( b , b ) tienen la unión f ( x , x ) y f ( x , y ) en la red de todos los términos y en la red de términos lineales, respectivamente. Como las operaciones de unión en general no concuerdan, la red de términos lineales no es propiamente hablando una subred de la red de todos los términos.
La unión y el encuentro de dos términos lineales propios [3] , es decir, su antiunificación y unificación, corresponden a la intersección y unión de sus conjuntos de caminos , respectivamente. Por lo tanto, cada subred de la red de términos lineales que no contiene Ω es isomorfa a una red de conjuntos y, por lo tanto, distributiva (véase la figura 5).
Al parecer, la red de subsunción fue investigada por primera vez por Gordon D. Plotkin , en 1970. [4]