Opis

• Tytuł:
  Discrete linear temporal logic with current time point clusters, deciding algorithms
• Twórca:
  Rybakov, V.
• Opis:
  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.
• Dostępność obiektu:
  Dostęp otwarty
• Prawa:
  Prawa autorskie (c) 2017 Logic and Logical Philosophy
• Data:
  2008.06.19
• Typ:
  info:eu-repo/semantics/article;
  info:eu-repo/semantics/publishedVersion
• Język:
  angielski
• Źródło:
  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
• Wydawca:
  Uniwersytet Mikołaja Kopernika w Toruniu
• Relacja: https://apcz.umk.pl/LLP/article/view/LLP.2008.009/1306
• Temat i słowa kluczowe:
  temporal logics;
  linear temporal logics;
  algorithms;
  Kripke structures;
  multi-modal logics;
  decidability;
  admissible inference rules
• Identyfikator: https://apcz.umk.pl/LLP/article/view/LLP.2008.009
• Dostawca danych:
  Akademicka Platforma Czasopism
• Czy mogę z tego obiektu skorzystać?:
  poproś o pozwolenie
• Rodzaj zawartości:
  teksty