I'm a beginner to this. Can anyone please point me to any resources for studying about equational logic, preferably with some example proofs to wet my feet in? Thanks in advance!
-
1$\begingroup$ Well, I'd hope you already found mathworld.wolfram.com/EquationalLogic.html . $\endgroup$– user5810Commented Jan 13, 2011 at 18:09
-
5$\begingroup$ To my mind, equational logic is very closely aligned with universal algebra, so this may give some more search terms. $\endgroup$– Todd TrimbleCommented Jan 13, 2011 at 18:56
2 Answers
Beyond what is taught in (American) high school algebra courses, I don't really know any beginner level treatments on equational logic. The link Ricky Demer provides a brief bibliography which includes a book on Universal Algebra and one on Mathematical Logic; browsing through your local university math library should have similar books on the same shelf that might be helpful. George Graetzer and McKenzie, McNulty, and Taylor are authors of two more books on Universal Algebra which contain a bit of equational logic, but do not say much about it as a proof system. Their focus is on Birkhoff's preservation theorem (HSP theorem) which is the main reason universal algebraists have for studying equational logic. (There are people in Theoretical Computer Science and other disciplines who have different reasons, e.g. term-rewriting systems. My exposure to Universal Algebra was more model-theoretic and not so much proof-theoretic.) I do not remember enough of the undergraduate literature to say what mathematical logic texts cover equational logic; there may be some computer science texts which do, in which case an internet book search may be more fruitful.
In addition George McNulty wrote a sort of primer in Equational Logic. Once you are familiar with the basic mechanics and want to know what recent research and work (within the last 25 years) that deals with equational logic, his survey is quite approachable.
Gerhard "Ask Me About System Design" Paseman, 2011.01.13
Look up:
- Term Rewriting systems and Knuth-Bendix completion
- theory of equations and solving systems of multivariate polynomials (Groebner Bases)
Though the latter subject, solving systems of equations over more concrete domains like fields, sounds very different from the purely syntactic manipulation in rewrite systems, the similarities are very astounding.