Reasoning About Knowledge Using Extensional Logics

Abstract

When representing statements about knowledge in a extensional logic, it occasionally happens that undesired conclusions arise. Such extraneous conclusions are often the result of substitution of equals for equals or existential instantiation within intensional operators such as Know. In the past, efforts at solving this problem have centered on modifications to the logic. In this thesis, I propose a solution that leaves the logic intact and changes the representation of the statements instead. The solution presented here has four main points: 1) Only propositions can be known. 2) Relations rather than functions should be used to describe objects. 3) Temporal reasoning is often necessary to represent many real-world problems. 4) In cases where more than one label can apply to the same object, an agent's knowledge about labels must be explicitly represented. When these guidelines are followed, statements about knowledge can be represented in standard first-order predicate logic in such a way that extraneous conclusions cannot be drawn. Standard first-order theorem provers (like Prolog) can then be used to solve problems which involve reasoning about knowledge.