ALEKS (http://www.aleks.com/) is a good way of learning procedural math, because it is very systematic and forces you to master the dependencies of a kind of problem before working on that kind of problem itself. Also the interface is very clean and user-friendly.
The method of ALEKS seems especially well-suited to introductory logic (truth tables, symbolizing English sentences, truth trees, proofs in SL or PL, etc.), but ALEKS doesn't have a logic program. Has anyone else made something like this?
(Note: I asked this question on math.SE and nobody has answered it for a long time so I'm asking it here. Here is the link to the post on math.SE: https://math.stackexchange.com/questions/722363/is-there-a-program-like-aleks-for-mathematical-logic)