Description

• Title:
  Discrete linear temporal logic with current time point clusters, deciding algorithms
• Creator:
  Rybakov, V.
• Description:
  The paper studies the logic TL(N\Box+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities \Diamond+ (possible in future) and \Diamond- (possible in past) and special temporal operations, – \Box+w (weakly necessary in future) and \Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(N\Box+-wC), so we prove that TL(N\Box+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(N\Box+-wC) and show how to reduce the problem for admissibility to the decidability of TL(N\Box+-wC) itself using definable universal modalities.
• Object availability:
  free access
• Rights:
  Prawa autorskie (c) 2017 Logic and Logical Philosophy
• Date:
  2008.06.19
• Type:
  info:eu-repo/semantics/article;
  info:eu-repo/semantics/publishedVersion
• Language:
  English
• Source:
  Logic and Logical Philosophy; Vol. 17 No. 1-2 (2008); 143-161;
  Logic and Logical Philosophy; Tom 17 Nr 1-2 (2008); 143-161;
  2300-9802;
  1425-3305
• Format:
  application/pdf
• Publisher:
  Uniwersytet Mikołaja Kopernika w Toruniu
• Relation: https://apcz.umk.pl/LLP/article/view/LLP.2008.009/1306
• Subject:
  temporal logics;
  linear temporal logics;
  algorithms;
  Kripke structures;
  multi-modal logics;
  decidability;
  admissible inference rules
• Identifier: https://apcz.umk.pl/LLP/article/view/LLP.2008.009
• Data provider:
  Akademicka Platforma Czasopism
• Can I use it?:
  seek permission
• Type:
  text