Módulo de unificación aritmética pre-hamburguesa y otras teorías decidibles

Abstract

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.