Where can I find the formal semantics of CycL defined?  I've looked over the documentation at www.opencyc.org, and it describes the semantics only rather vaguely and informally. The OE manual pays a lot of attention to syntax, but says very little about semantics.  Nor have I had any luck searching on Google for any paper giving CycL's formal semantics.

The reason I ask is because CycL isn't *quite* first-order predicate logic... and I want to understand exactly how it differs.  For example, what semantic significance (affecting the meanings of sentences) do argument-type assertions have?  What is the real difference between a collection and a set? (The tutorial mentions that sets are defined by extension, whereas collections are defined by extension... but doesn't explain this with any precision.)