@MISC{LTLAXIO5.MIZ,
  AUTHOR = {Giero, Mariusz},
  TITLE = {Propositional Linear Time Temporal Logic with Initial Semantics},
  SECTION1 = {Preliminaries},
  SECTION2 = {Initial validity semantics - definitions},
  SECTION3 = {The connections between normal semantics and initial semantics},
  SECTION4 = {A formal system (Hilbert-like) for LTLB with initial semantics},
  SECTION5 = {Soundness Theorem for LTLB with initial semantics},
  SECTION6 = {Weak Completeness Theorem for LTLB with initial semantics},
  SECTION7 = {Deduction Theorem},
  SECTION8 = {The connections between derivability in the formal system for LTLB with normal semantics
	and the formal system for LTLB with initial semantics},
  DAY = {22},
  MONTH = {October},
  YEAR = {2015},
  ADDRESS1 = {Faculty of Economics and Informatics in Vilnius\\ University of Bia{\l}ystok\\
  Kalvariju 135, LT-08221 Vilnius\\ Lithuania},
  SUMMARY = {In article \cite{LTLAXIO1.ABS} a formal system for Propositional Linear Temporal Logic
	(in short LTLB) with normal semantics was introduced. The language of this logic consists of
	``until" operator in very strict version. The very strict ``until" operator enables to express
	all other temporal operators. In this article we construct a formal system for LTLB with
	the initial semantics \cite{KroMer}. Initial semantics means that we define the validity
	of formula in model as satisfaction of formula in the initial state of model only instead of
	satisfaction in all states of model. We prove the Deduction Theorem,
        and soundness and completeness of the introduced formal system.
        We also prove some theorems to compare both formal systems,
	i.e., the one introduced in the article \cite{LTLAXIO1.ABS}
        and the one introduced in this article.
	Formal systems for temporal logics are applied in verification of
        computer programs. In order to carry out the verification one
        has to derive an appropriate formula within selected formal
	system. The formal systems introduced in \cite{LTLAXIO1.ABS}
        and in this article can be used to carry out such verifications
        in Mizar.}}

@BOOK{KroMer,
 AUTHOR={Kr\"oger, Fred and Merz, Stephan},
 TITLE={Temporal Logic and State Systems},
 PUBLISHER={Springer-Verlag},
 YEAR={2008}}

