SEM: Formalization exercise

As an exercise I formalized one of Peter's earlier versions of OWL in the
ACL2 logic.  Mostly this was for my own edification.  But a document
describing the result is attached.
 
One result of this exercise is that we can be assured that there exists an
interpretation (a set of values for EXT, CEXT, etc.) that satisfies the
axioms as stated in the original document (subject to the notes on
completeness).
 
- Mike
 
Michael K. Smith
EDS Austin Innovation Centre
98 San Jacinto, #500
Austin, TX 78701
512 404-6683