| Abstract [eng] |
Modal logic is obtained by extending classical logic with modality operators. Temporal logic is obtained by extending classical logic with temporal operators. This paper deals with linear temporal logic. The work objective is to distinguish fragments of linear time logic and construct efficient sequential calculi for them. There are three most widely known sequent calculi for linear temporal logic: infinite, invariant rule, and cyclic type. The main results of this work are the definition of a unary fragment of linear temporal logic, and the definition and proof of auxiliary lemmas for sequent calculus in linear temporal logic. A new sequent calculus for linear temporal logic has been developed, which does not use cycle detection in proof search and is more efficient than the classical sequent calculus in the defined fragment. The equivalence between the newly developed sequent calculi and the classical sequent calculus for linear temporal logic in the defined fragment has been proved. |
