Desunificación

La desunificación , en informática y lógica , es un proceso algorítmico para resolver inecuaciones entre expresiones simbólicas .

• Alain Colmerauer (1984). "Ecuaciones e inecuaciones en árboles finitos e infinitos". En ICOT (ed.). Actas de la Conferencia Internacional sobre Sistemas Informáticos de Quinta Generación . págs. 85–99 . 
• Hubert Comon (1986). "Completitud suficiente, sistemas de reescritura de términos y 'anti-unificación'"". Actas de la 8.ª Conferencia Internacional sobre Deducción Automatizada . LNCS . Vol.  230. Springer. págs. 128–140 . "Anti-unificación" aquí se refiere a la resolución de inecuaciones, una denominación que hoy en día se ha vuelto bastante inusual, cf. Anti-unificación (ciencia de la computación) .
• Claudio Kirchner; Pierre Lescanne (1987). "Resolviendo Disecuaciones". Proc. LIC . págs. 347-352 . 
• Claude Kirchner y Pierre Lescanne (1987). Resolución de disecuaciones (Informe de investigación). INRIA.
• Hubert Comon (1988). Unificación y desunificación: Théorie et aplicaciones (PDF) (Ph.D.). INP de Grenoble.
• Hubert Comon; Pierre Lescanne (marzo-abril de 1989). "Problemas ecuacionales y desunificación" . J. Symb. Comput. 7 ( 3-4 ): 371-425 . CiteSeerX 10.1.1.139.4769 . doi : 10.1016/S0747-7171(89)80017-3 . 
• Comon, Hubert (1990). "Fórmulas ecuacionales en álgebras ordenadas". Proc. ICALP .Comon demuestra que la teoría de la lógica de primer orden sobre la igualdad y la pertenencia a un tipo es decidible; es decir, cada fórmula de lógica de primer orden construida a partir de símbolos de función arbitrarios, "=" y "∈", pero ningún otro predicado, puede probarse o refutarse eficazmente. Mediante la negación lógica (¬), la no igualdad (≠) puede expresarse en fórmulas, pero las relaciones de orden (<) no. Como aplicación, demuestra la completitud suficiente de los sistemas de reescritura de términos .
• Hubert Comon (1991). "Desunificación: una revisión" . En Jean-Louis Lassez; Gordon Plotkin (eds.). Lógica computacional: ensayos en honor de Alan Robinson . MIT Press. págs. 322–359 . 
• Hubert Comon (1993). "Axiomatizaciones completas de algunas álgebras de términos cociente" ( PDF) . Actas del 18.º Coloquio Internacional sobre Autómatas, Lenguajes y Programación . LNCS. Vol.  510. Springer. págs. 148–164 . Consultado el 29 de junio de 2013 . 

• Unificación (informática) : resolución de ecuaciones entre expresiones simbólicas.
• Programación lógica con restricciones : incorporación de algoritmos de resolución para clases particulares de desigualdades (y otras relaciones) en Prolog.
• Programación con restricciones : resolución de algoritmos para clases particulares de desigualdades.
• Algoritmo simplex : algoritmo para resolver inecuaciones lineales
• Inecuación : tipos de inecuaciones en matemáticas en general, incluyendo una breve sección sobre su resolución.
• Resolución de ecuaciones : cómo resolver ecuaciones en matemáticas