@book(spatial_logic_handbook,
 editor       = {M. Aiello and Pratt-Hartmann, I. and {van Benthem}, J.},
 year         = {2007},
 title        = {Handbook of Spatial Logics},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4020-5587-4},
)
@inproceedings(DBLP:conf/lpar/ArtaleKRZ13,
 author       = {A. Artale and R. Kontchakov and V. Ryzhikov and M. Zakharyaschev},
 year         = {2013},
 title        = {The Complexity of Clausal Fragments of {LTL}},
 booktitle    = {Proc. of LPAR 2013},
 series       = {LNCS},
 volume       = {8312},
 publisher    = {Springer},
 pages        = {35--52},
 doi          = {10.1007/978-3-642-45221-5\_3},
)
@article(DBLP:journals/tocl/ArtaleKRZ14,
 author       = {A. Artale and R. Kontchakov and V. Ryzhikov and M. Zakharyaschev},
 year         = {2014},
 title        = {A Cookbook for Temporal Conceptual Data Modelling with Description Logics},
 journal      = {{ACM} Transactions on Computational Logic},
 volume       = {15},
 number       = {3},
 pages        = {1--50},
 doi          = {10.1145/2629565},
)
@inproceedings(artale2015,
 author       = {A. Artale and R. Kontchakov and V. Ryzhikov and M. Zakharyaschev},
 year         = {2015},
 title        = {Tractable Interval Temporal Propositional and Description Logics},
 booktitle    = {Proc. of AAAI 2015},
 publisher    = {{AAAI} Press},
 pages        = {1417--1423},
)
@article(asp79,
 author       = {B. Aspvall and M. F. Plass and R. E. Tarjan},
 year         = {1979},
 title        = {A Linear Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas},
 journal      = {Information Processing Letters},
 volume       = {8},
 number       = {3},
 pages        = {121--123},
 doi          = {10.1016/0020-0190(79)90002-4},
)
@book(Baader:2003:DLH:885746,
 editor       = {F. Baader and D. Calvanese and D.L. McGuinness and D. Nardi and Patel-Schneider, P.F.},
 year         = {2003},
 title        = {The Description Logic Handbook: Theory, Implementation, and Applications},
 publisher    = {Cambridge University Press},
 doi          = {10.2277/0521781760},
)
@book(modal-logic,
 author       = {P. Blackburn and M. de Rijke and Y. Venema},
 year         = {2002},
 title        = {Modal Logic},
 publisher    = {Cambridge University Press},
)
@article(DBLP:journals/jcss/BloemJPPS12,
 author       = {R. Bloem and B. Jobstmann and N. Piterman and A. Pnueli and Y. Sa'ar},
 year         = {2012},
 title        = {Synthesis of Reactive(1) Designs},
 journal      = {Journal of Computer and System Sciences},
 volume       = {78},
 number       = {3},
 pages        = {911--938},
 doi          = {10.1016/j.jcss.2011.08.007},
)
@unpublished(bresolin:2016,
 author       = {D. Bresolin and A. Kurucz and Mu{\~n}oz-Velasco, E. and V. Ryzhikov and G. Sciavicco and M. Zakharyaschev},
 year         = {2016},
 title        = {Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report)},
 url          = {http://arxiv.org/abs/1604.03515v1},
 note         = {Preliminary version},
)
@inproceedings(DBLP:conf/jelia/BresolinMS14,
 author       = {D. Bresolin and Mu{\~{n}}oz{-}Velasco, E. and G. Sciavicco},
 year         = {2014},
 title        = {Sub-propositional Fragments of the Interval Temporal Logic of {A}llen's Relations},
 booktitle    = {Proc. of JELIA 2014},
 series       = {LNCS},
 volume       = {8761},
 publisher    = {Springer},
 pages        = {122--136},
 doi          = {10.1007/978-3-319-11558-0\_9},
)
@article(ChenLin93,
 author       = {C.C. Chen and I.P. Lin},
 year         = {1993},
 title        = {The computational complexity of satisfiability of temporal {Horn} formulas in propositional linear-time temporal logic},
 journal      = {Information Processing Letters},
 volume       = {45},
 number       = {3},
 pages        = {131--136},
 doi          = {10.1016/0020-0190(93)90014-Z},
)
@article(ChenLin94,
 author       = {C.C. Chen and I.P. Lin},
 year         = {1994},
 title        = {The Computational Complexity of the Satisfiability of Modal Horn Clauses for Modal Propositional Logics},
 journal      = {Theoretical Computer Science},
 volume       = {129},
 number       = {1},
 pages        = {95--121},
 doi          = {10.1016/0304-3975(94)90082-5},
)
@book(cookhorn,
 author       = {S. Cook and P. Nguyen},
 year         = {2010},
 title        = {Logical foundations of proof complexity},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511676277},
)
@article(del1987note,
 author       = {{Fari{\~n}as Del Cerro}, L. and M. Penttonen},
 year         = {1987},
 title        = {A note on the complexity of the satisfiability of modal {H}orn clauses},
 journal      = {Journal of Logic Programming},
 volume       = {4},
 number       = {1},
 pages        = {1--10},
 doi          = {10.1016/0743-1066(87)90018-5},
)
@book(temporal_logic_foundations,
 author       = {D. Gabbay and I. Hodkinson and M. Reynolds},
 year         = {1994},
 title        = {Temporal Logic: mathematical foundations and computational aspects, Volume 1},
 series       = {Oxford Logic Guides},
 publisher    = {Oxford University Press},
)
@article(interval_modal_logic,
 author       = {J.Y. Halpern and Y. Shoham},
 year         = {1991},
 title        = {A Propositional Modal Logic of Time Intervals},
 journal      = {Journal of the ACM},
 volume       = {38},
 pages        = {279--292},
 doi          = {10.1145/115234.115351},
)
@article(horn,
 author       = {A. Horn},
 year         = {1951},
 title        = {On Sentences Which Are True of Direct Unions of Algebras},
 journal      = {Journal of Symbolic Logic},
 volume       = {16},
 number       = {1},
 pages        = {14--21},
 doi          = {10.2307/2268661},
)
@inproceedings(DBLP:conf/dlog/KonevLWZ15,
 author       = {B. Konev and C. Lutz and F. Wolter and M. Zakharyaschev},
 year         = {2015},
 title        = {Conservative Rewritability of Description Logic TBoxes: First Results},
 booktitle    = {Proc. of the 28th DL Workshop},
 series       = {CEUR-WS.org},
 volume       = {1350},
 pages        = {196 -- 207},
)
@article(krom,
 author       = {M.R. Krom},
 year         = {1970},
 title        = {The Decision Problem for Formulas in Prenex Conjunctive Normal Form with Binary Disjunction},
 journal      = {Journal of Symbolic Logic},
 volume       = {35},
 number       = {2},
 pages        = {14--21},
 doi          = {10.2307/2270511},
)
@article(nguyen2004complexity,
 author       = {L.A. Nguyen},
 year         = {2004},
 title        = {On the complexity of fragments of modal logics},
 journal      = {Advances in Modal Logic},
 volume       = {5},
 pages        = {318--330},
)
@book(papa,
 author       = {C.H. Papadimitriou},
 year         = {1994},
 title        = {Computational Complexity},
 publisher    = {Addison Wesley},
)