Sentential theories of belief hold that propositions (the things that agents believe and know) are sentences of a representation language. To analyze quantification into the scope of attitudes, these theories require a naming map a function that maps objects to their names in the representation language. Epistemic logics based on sentential theories usually assume a single naming map, which is built into the logic. I argue that to describe everyday knowledge, the user of the logic must be able to define new naming maps for particular problems. Since the range of a naming map is usually an infinite set of names, defining a map requires quantification over names. This paper describes an epistemic logic with quantification over names, presents a theorem‐proving algorithm based on translation to first‐order logic, and proves soundness and completeness. The first version of the logic suffers from the problem of logical omniscience; a second version avoids this problem, and soundness and completeness are proved for this version also.

Finding the referent of a definite noun phrase is a classic problem in natural language processing. Most work assumes that when a program begins to analyze an utterance, it already has the knowledge it needs for identifying referents. If a robot accepts commands in natural language, this assumption may not hold. Suppose a user says, “Go get the book on the table in room 3,” but the robot has never been in room 3, so it lacks the knowledge it needs to identify the referent of “the book on the table in room 3.” To gain this knowledge, the robot must travel to room 3 and search. This article describes a simulated robot that accepts commands in English and actively searches for the referents of definite descriptions.

The offline parsable grammars apparently have enough formal power to describe human language, yet the parsing problem for these grammars is solvable. Unfortunately they exclude grammars that use x-bar theory - and these grammars have strong linguistic justification. We define a more general class of unification grammars, which admits x-bar grammars while preserving the desirable properties of offline parsable grammars.