Encoding propositional logic

[gmhwxi]

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.