Dense Time Logic Programming

In this paper, we describe a dense temporal logic programming (DTLP) framework based on infinite binary trees calledomega trees. We then look at an important subset of omega trees calledordinaltreesthat represent only meaningful dense time models. Ordinal trees have the properties ofstabilityandrecurrence, which allow them to be represented finitely. The finite representations calledordinalstructurescan be used as temporal data structures and its nodes can be labelled with formulae, giving us the basis for modeling temporally located information. In this paper, we label ordinal structure nodes with Prolog clauses to gettemporal horn clausesthat represent temporal facts, rules and queries. Temporal resolution tries to prove temporal queries from a set of temporal facts and rules using a process calledaligningwhich provides the counterpart of the conventional unification algorithm. Aligning restructures ordinal trees to facilitate the transfer of temporal information between them. We present theoretical results to show that aligning is computable, and that the procedures for aligning and resolution are correct.