
25 Apr
2012
25 Apr
'12
7:09 p.m.
I uploaded a new version of the ACU unifier in package cmu. It includes a Linear Diaphantine equation solver that now handles inhomogeneous equations. What's interesting is the algorithm is based on a paper by Contejean and Devie. That paper includes a proof of correctness of their algorithm. Yet I found an example in which following the steps in the order they gave, the algorithm produces extra answers. I had to switch the order of the steps in the algorithm to get the right answer. I wonder if anyone else knows of this issue. The example is given in the module documentation on Hackage. John http://hackage.haskell.org/packages/archive/cmu/1.6/doc/html/Algebra-Commuta...