Linear Non-Transitive Temporal Logic, Knowledge Operations, Algorithms for Admissibility

TL;DR

This paper explores the satisfiability, decidability, and admissibility of inference rules in non-transitive linear temporal logic, introducing algorithms and formalizations for knowledge within this framework, notably proving decidability of admissibility.

Contribution

It introduces algorithms for key problems in non-transitive linear temporal logic and establishes the decidability of admissibility, advancing formalizations of knowledge in this context.

Findings

Decidability of admissibility in LTL(Past,m)

Algorithms for satisfiability and admissibility problems

Formalizations of knowledge in non-transitive temporal logic

Abstract

The paper studies problems of satisfiability, decidability and admissibility of inference rules, conceptions of knowledge and agent's knowledge in non-transitive temporal linear logic LTL(Past,m). We find algorithms solving mentioned problems, justify our approach to consider linear non-transitive time with several examples. Main, most complicated, technical new result is decidability of LTL(Past,m) w.r.t. admissible rules. We discuss several ways to formalize conceptions of knowledge and agent's knowledge within given approach in non-transitive linear logic with models directed to past.