<p>We consider backward proof search of sequents of propositional linear discrete tense logic with unary temporal operators. The backward proof search involves derivation loop checks (DLC). We present a strategy for DLC directed toward reduction of the loop checks on branches of backward proof search trees.</p>

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

Global condition check strategy for a cyclic sequent calculus of temporal logic

  • Romas Alonderis,
  • Aida Pliuškevičienė,
  • Haroldas Giedra

摘要

We consider backward proof search of sequents of propositional linear discrete tense logic with unary temporal operators. The backward proof search involves derivation loop checks (DLC). We present a strategy for DLC directed toward reduction of the loop checks on branches of backward proof search trees.