Unification modulo presburger arithmetic and other decidable theories
We present a general uni cation algorithm modulo Presburger Arithmetic for a re- stricted class of modularly speci ed theories where function symbols of the target theory have non arithmetic codomain sorts. Additionally, we comment on conditions guaran-teeing decidability of matching and uni cation...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Universidad Autónoma de Bucaramanga
2001-12-01
|
| Series: | Revista Colombiana de Computación |
| Online Access: | https://revistas.unab.edu.co/index.php/rcc/article/view/1112 |