A metalogic programming approach to reasoning about time in knowledge bases

The problem of representing and reasoning about two notions of time that are relevant in the context of knowledge bases is addressed. These are called historical time and belief time respectively. Historical time denotes the time for which information models reality/Belief time denotes the time lor which a belief is held (by an agent or a knowledge base). We formalize an appropriate theory of time using logic as a meta-language. We then present a metalogic program derived from this theory through fold/unfold transformations. The metalogic program enables the temporal reasoning required for knowledge base applications to be carried out efficiently. The metalogic program is directly implementable as a Prolog program and hence the need for a more complex theorem prover is obviated. The approach is applicable for such knowledge base applications as legislation and legal reasoning and in the context of multi-agent reasoning where an agent reasons about the beliefs of another agent.