Scholarlink

<p>We consider the first-order theory of order over real numbers extended with monadic uninterpreted predicates. It has long been established that this theory is decidable, by different approaches such as a reduction to linear-time temporal logic over the reals, expressing the problem as a particular case of deciding the first-order theory of all linear orderings, or reasoning about restrictions of the monadic second-order theory of order. The main contribution of this work is to provide a complete self-contained proof of decidability for this logic. Additionally, our proof develops a symbolic notation system for models of satisfiable formulas, which can be seen as a first step towards an actual implementation of a decision procedure for the theory of order over the reals.</p>

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

On the Theory of Order Over Real Numbers

  • 期刊论文

  • 发表日期：

    2026年4月3日

查看全文
  • Bernard Boigelot,
  • Pascal Fontaine,
  • Baptiste Vergain

摘要

We consider the first-order theory of order over real numbers extended with monadic uninterpreted predicates. It has long been established that this theory is decidable, by different approaches such as a reduction to linear-time temporal logic over the reals, expressing the problem as a particular case of deciding the first-order theory of all linear orderings, or reasoning about restrictions of the monadic second-order theory of order. The main contribution of this work is to provide a complete self-contained proof of decidability for this logic. Additionally, our proof develops a symbolic notation system for models of satisfiable formulas, which can be seen as a first step towards an actual implementation of a decision procedure for the theory of order over the reals.