Technical Report: DCC-97-15

On Diophantine systems coming from AC-unification of higher-order patterns: exploiting symmetries

Ana Paula Tomás, Evelyne Contejean

Departamento de Ciência de Computadores & LIACC
Faculdade de Ciências, Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal

December 1997


Abstract

We study systems of linear Diophantine equations that arise when performing AC-unification of higher-order patterns by the algorithm recently proposed by A. Boudet and E. Contejean. Their solution space presents symmetries which can be exploited to solve them more efficiently.

Keywords: Linear Diophantine Systems.