Linear temporal logic LTL: basis for admissible rules
S Babenyshev, V Rybakov - Journal of Logic and Computation, 2011 - academic.oup.com
S Babenyshev, V Rybakov
Journal of Logic and Computation, 2011•academic.oup.comThe object of our study is the propositional linear temporal logic LTL with operations Until
and Next. We deal with inference rules admissible in LTL. Earlier the decidability of LTLw. rt
to admissibility was shown. That, in particular, allowed to suggest a recursive infinite basis
for admissible rules. However, that result gives no information about the structure and
properties of such basis, thereby not allowing to use it for inferences. The current article aims
to cover this gap and to provide an explicit (infinite) basis for rules admissible in LTL.
and Next. We deal with inference rules admissible in LTL. Earlier the decidability of LTLw. rt
to admissibility was shown. That, in particular, allowed to suggest a recursive infinite basis
for admissible rules. However, that result gives no information about the structure and
properties of such basis, thereby not allowing to use it for inferences. The current article aims
to cover this gap and to provide an explicit (infinite) basis for rules admissible in LTL.
Abstract
The object of our study is the propositional linear temporal logic LTL with operations Until and Next.We deal with inference rules admissible in LTL. Earlier the decidability of LTLw.r.t. to admissibility was shown. That, in particular, allowed to suggest a recursive infinite basis for admissible rules. However, that result gives no information about the structure and properties of such basis, thereby not allowing to use it for inferences. The current article aims to cover this gap and to provide an explicit (infinite) basis for rules admissible in LTL.
Oxford University Press以上显示的是最相近的搜索结果。 查看全部搜索结果