Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles
Fecha
2001-12-01Registro en:
2539-2115
1657-2831
instname:Universidad Autónoma de Bucaramanga UNAB
Autor
Ayala Rincón, Mauricio
Tavares Araújo, Ivan E.
Resumen
Presentamos un algoritmo de unificación general módulo Presburger Arithmetic para una clase restringida de teorías especificadas modularmente donde los símbolos de función de la teoría objetivo tienen clases de codominio no aritméticas. Además, comentamos las condiciones que garantizan la decidibilidad de problemas de emparejamiento y unificación módulo teorías más generales que las aritméticas, que aparecen cuando se implementa la deducción automática combinando técnicas de reescritura condicional y algoritmos de decisión para predicados incorporados.