> I'm not going to summarize classic equational reasoning (with it's deep connection to algebraic geometry and whatnot) here in a single HN post ;)
Aw :(
Alright, I'll just chase down some of the references you say. I was going to check out Prolog 2 anyway, after browsing the wikipedia article on Colmerauer a few days ago and seeing a reference to his later work there.
To be a bit more concrete than the grandparent's name soup, I liked this handbook article about unification in theories: Franz Baader and Jörg Siekmann. Unification Theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
Comments
Aw :(
Alright, I'll just chase down some of the references you say. I was going to check out Prolog 2 anyway, after browsing the wikipedia article on Colmerauer a few days ago and seeing a reference to his later work there.
To be a bit more concrete than the grandparent's name soup, I liked this handbook article about unification in theories: Franz Baader and Jörg Siekmann. Unification Theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
This seems to be a newer version with similar contents but different authors: http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
This is specific to unification and not to broader equational reasoning.
Thanks.