On Temporal References via Definite Descriptions in First-Order Monadic Logic of Order
摘要
Temporal reference, understood as the capability of referring to particular points of time, is an essential aspect of temporal reasoning. In this paper we model it with the definite description (iota) operator added to first-order monadic logic of order—a standard formalism for reasoning about time. This allows us to express temporal reference directly and with dedicated tools, which is of particular importance from the point of view of proof systems for automated reasoning. We construct a sound and complete tableau system, as well as provide complexity results for the satisfiability problem of the obtained logic.