• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of applied non-classical logics >Back from the future
【24h】

Back from the future

机译：从未来回来

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

abstract. Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: AUB holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and w. This "ambivalent" nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until by introducing a new temporal operator V that allows us to formalize the "history" of until, i.e., the "internal" universal quantification over the time instants between the current one and w'. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N(LTLv) for a linear-time logic LTLv endowed with the new history operator. We show that LTLv is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTLv into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTLv formulas.
机译：抽象。直到是一个众所周知的困难的时间算子，因为它同时存在和普遍存在：AUB在当前时刻w成立，而B要么在w持有，要么在将来存在B的时刻w'，这样A在当前时刻和w之间的所有时刻保持不变。当试图给出直到的推导规则时，这种“矛盾的”性质构成了重大挑战。相反，在本文中，我们通过引入新的时间运算符V来明确to的这种对偶性，从而使我们能够规范to的“历史”，即在当前时间与当前时间之间的瞬间的“内部”通用量化。 w'。该方法为形式化直到〜运算符赋予的时间逻辑的演绎系统提供了基础。为了具体起见，我们在这里为带有新历史运算符的线性时间逻辑LTLv给出一个标记的自然推导系统N（LTLv）。我们显示LTLv等同于线性时态逻辑LTL，具有直到，这是通过形式化两个逻辑之间的来回转换来实现的。我们还使用过去的运算符通过时间逻辑定义了从LTLv到LTL的间接转换。这样的结果为LTLv公式的可满足性问题提供了一个上限。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号