A name created by a logical event
Examples: assoc caddr + "ACL2-USER" :here
A logical name is either a name introduced by some event, such as defun, defthm, or defpkg, or else is the keyword
Logical names are used primarily in the theory manipulation functions, e.g., universal-theory and current-theory with which you may obtain some standard theories as of some point in the historical past. The reference points are the introductions of logical names, i.e., the past is determined by the events it contains. One might ask, ``Why not discuss the past with the much more flexible language of command descriptors?'' (See command-descriptor.) The reason is that inside of such events as encapsulate or macro commands that expand to progns of events, command descriptors provide too coarse a grain.
When logical names are used as referents in theory expressions used in books, one must consider the possibility that the defining event within the book in question becomes redundant by the definition of the name prior to the assumption of the book. See redundant-events.