Nice article, I do like the way it's explained in a way that a programmer like myself can understand it. I did note a few typos that I will take the opportunit

Nice article, I do like the way it's explained in a way that a programmer like myself can understand it. I did note a few typos that I will take the opportunity to report here, in order to make an already great article a little better: Under "PM-Lisp Axioms": Looking at the code "(when (or p q) (or (q p))". I don't think the (q p) should have parens around it. Under "(proves a b)": There is no ending quote at the end of the last sentence. Under "(subst a b c)": I find the text "PM-LIsp". I guess the I should be lower case.