@MISC{LTLAXIO1.MIZ,
  AUTHOR = {Giero, Mariusz},
  TITLE = {The Axiomatization of Propositional Linear Time Temporal Logic},
  ACKNOWLEDGEMENT = {The author would like
   to thank Professor Kazimierz Trz\c{e}sicki for his introduction
   to the topic and many useful comments.
   The author thanks Professor Andrzej Trybulec
   for encouragement to formalize this topic and many useful comments.
   The author also thanks Dr. Adam Naumowicz and Karol P\c{a}k for many
   useful comments and Dr. Adam Grabowski and Dr. Artur
   Korni{\l}owicz for answers to some vital questions.},
  SECTION1 = {Preliminaries},
  SECTION2 = {The Language. Basic Operators.
    Further Operators as Abbreviations},
  SECTION3 = {The Semantics},
  SECTION4 = {Validity. Consequence. Some Facts about the Semantical Notions},
  SECTION5 = {Axioms. Derivation Rules. Derivability.
    Soundness Theorem for LTL},
  SECTION6 = {Derivation of Some Formulas. Deduction Theorem of LTL},
  DAY = {20},
  MONTH = {November},
  YEAR = {2010},
  ADDRESS1 = {Institute of Sociology\\University of Bia{\l}ystok\\
  Plac Uniwersytecki 1, 15-420 Bia{\l}ystok\\Poland},
  SUMMARY = {The article introduces propositional linear time temporal logic
  as a formal system. Axioms and rules of derivation are defined.
  Soundness Theorem and Deduction Theorem are proved (\cite{KroMer}).}}

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

