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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On Temporal References via Definite Descriptions in First-Order Monadic Logic of Order

  • Andrzej Indrzejczak,
  • Przemysław Andrzej Wałęga,
  • Michał Zawidzki

摘要

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.