@MISC{LTLAXIO4.MIZ,
  AUTHOR = {Giero, Mariusz},
  TITLE = {Weak Completeness Theorem for Propositional Linear Time Temporal Logic},
  ACKNOWLEDGEMENT = {I would like to thank Prof. Dr. Stephan Merz
  for valuable hints which helped me to prove the theorem.
  I would particularly like to thank Dr. Artur Korni{\l}owicz who patiently
  answered a lot of my questions regarding writing this article.
  I would like to thank Dr. Josef Urban for discussions and
  encouragement to write the article.
  I would like to thank Prof. Andrzej Trybulec, Dr. Adam Naumowicz,
  Dr. Grzegorz Bancerek and Karol P\k{a}k for their help in preparation
  of the article.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Set of PNP-formulas. Completions of Formulas and PNPs.},
  SECTION3 = {Set of possible next-state PNPs},
  SECTION4 = {A PNP-Tree and Its Properties},
  SECTION5 = {A Path in PNP-Tree and Its Properties.
  Existence of Temporal Model for a Consistent PNP.
  Weak Completeness Theorem.}
  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 = {We prove weak (finite set of premises) completeness
  theorem for extended propositional linear time temporal logic
  with irreflexive version of until-operator. We base on
  the proof for basic propositional linear time temporal
  logic given in \cite{KroMer} which roughly follows the
  idea of Henkin-Hasenjaeger method for classical logic.
  We show that a temporal model exists for every formula which
  negation is not derivable (Satisfiability Theorem).
  The contrapositive of that theorem leads to derivability
  of every valid formula. We build a tree of consistent and
  complete~PNPs  which is used to construct the model.}}

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

