I turned some of my lecture notes into an article in the Effective-ATS
series:
http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/prop-logic/index.html
For someone interested in the theorem-proving aspect of ATS, this article
is a simple
starting point.