Global condition check strategy for a cyclic sequent calculus of temporal logic
摘要
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.