@MISC{LTLAXIO3.MIZ,
  AUTHOR = {Giero, Mariusz},
  TITLE = {The Properties of Sets of Temporal Logic Subformulas},
  ACKNOWLEDGEMENT = {I would like to thank Prof. Andrzej Trybulec,
  Dr. Artur Korni{\l}owicz, Dr. Adam Naumowicz and Karol P\c{a}k
  for their help in preparation of the article.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Set of Subformulas where an until-formula is treated as Indivisible and its Properties},
  SECTION3 = {Extended Set of Subformulas and its Properties},
  SECTION4 = {An Ordered Pair of Finite Sequences of Formulas (Positive-Negative Pair, for short PNP). PNP-formula, Consistent PNP and Complete PNP},
  SECTION5 = {The Properties of Consistent PNPs},
  DAY = {7},
  MONTH = {May},
  YEAR = {2012},
  ADDRESS1 = {Department of Logic, Informatics and Philosophy of Science\\University of Bia{\l}ystok\\
  Plac Uniwersytecki 1, 15-420 Bia{\l}ystok\\Poland},
  SUMMARY = {This is a second preliminary article to prove completeness
  theorem of propositional temporal logic. We introduce two modified
  definitions of a subformula. In the first one we treat until-formula
  as indivisible. In the second one we extend set
  of subformulas of until-formulas by special disjunctive formula.
  This is needed to construct a temporal model. We also define
  an ordered positive-negative pair of finite sequences of formulas
  (PNP). PNPs represent states of a temporal model.}}

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

