An Epistemic Logic with Quantification over Names

Contents

Quantification into the scope of attitudes is arguably the hardest problem in the study of propositional attitudes. It seems clear that to analyze this phenomenon in a sentential theory, we need a mapping from objects to their names in the representation language. The philosophical work of the last fifteen years has established that there is no universal mapping from objects to names - an object can have more than one useful name, and which one we want depends on our goals. Haas expressed similar ideas, without offering any proposals for implementation. In the meantime, AI workers have been trying to find resolution theorem provers for epistemic logics. The logics they work on include only trivial treatments of quantification into the scope of attitudes. Konolige simply postulates a class of distinguished constants. His notation cannot express any theory about these constants, nor is there any theory built into the formalism. I have proposed a logic that allows the user to define the naming maps that are needed for particular domains. This logic does not solve the problem, but it allows us to express the kind of knowledge that is needed for a solution. It also allows for a resolution theorem-proving algorithm, and even for a straightforward (though incomplete) Prolog implementation.