@inproceedings(BB-ECTLplus-strategies,
 author       = {Artie Basukoski and Alexander Bolotov},
 year         = {2005},
 title        = {Search Strategies for Resolution in CTL-Type Logics: Extension and Complexity},
 booktitle    = {12th International Symposium on Temporal Representation and Reasoning (TIME 2005)},
 pages        = {195--197},
 doi          = {10.1109/TIME.2005.32},
)
@phdthesis(Bolotov-phd,
 author       = {Alexander Bolotov},
 year         = {2000},
 title        = {Clausal Resolution for Branching-Time Temporal Logic.},
 school       = {Department of Computing and Mathematics, The Manchester Metropolitan University},
)
@article(BB-ECTLplus-journal,
 author       = {Alexander Bolotov and Artie Basukoski},
 year         = {2006},
 title        = {A Clausal Resolution Method for Branching-Time Logic ECTL+},
 journal      = {Annals of Mathematics and Artificial Intelligence},
 volume       = {46},
 number       = {3},
 pages        = {235\IeC{\textendash}263},
 doi          = {10.1007/s10472-006-9018-1},
)
@article(BB-jal,
 author       = {Alexander Bolotov and Artie Basukoski},
 year         = {2006},
 title        = {A Clausal Resolution Method for Extended Computation Tree Logic {ECTL}},
 journal      = {Journal of Applied Logic},
 volume       = {4},
 number       = {2},
 pages        = {141--167},
 doi          = {10.1016/j.jal.2005.06.003},
)
@inproceedings(BD00,
 author       = {Alexander Bolotov and Clare Dixon},
 year         = {2000},
 title        = {Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule},
 booktitle    = {Seventh International Workshop on Temporal Representation and Reasoning, {TIME} 2000, Nova Scotia, Canada, July 7-9, 2000},
 publisher    = {{IEEE} Computer Society},
 pages        = {163--172},
 doi          = {10.1109/TIME.2000.856598},
)
@article(BF99,
 author       = {Alexander Bolotov and Michael Fisher},
 year         = {1999},
 title        = {A Clausal Resolution Method for {C}{T}{L} Branching-time Temporal Logic},
 journal      = {Journal of experimental and theoretical artificial intelligence},
 volume       = {11},
 number       = {1},
 pages        = {77--93},
 doi          = {10.1080/095281399146625},
)
@article(BFD02,
 author       = {Alexander Bolotov and Michael Fisher and Clare Dixon},
 year         = {2002},
 title        = {On the Relationship between w-automata and Temporal Logic Normal Forms},
 journal      = {Journal of Logic and Computation},
 volume       = {12},
 number       = {4},
 pages        = {561--581},
 doi          = {10.1093/logcom/12.4.561},
)
@inproceedings(pltl-invariants-fisher,
 author       = {James Brotherston and Anatoli Degtyarev and Michael Fisher and Alexei Lisitsa},
 year         = {2002},
 title        = {Searching for Invariants Using Temporal Resolution},
 editor       = {Matthias Baaz and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, {LPAR} 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2514},
 publisher    = {Springer},
 pages        = {86--101},
 doi          = {10.1007/3-540-36078-6\_6},
)
@inproceedings(Buc62,
 author       = {Julius Richard B\"{u}chi},
 year         = {1962},
 title        = {On a Decision Method in Restricted Second-order Arithmetics},
 booktitle    = {Proceedings of the International Congress of Logic, Methodology and Philosophy of Science},
 publisher    = {Stanford University Press},
 pages        = {1--12},
)
@inproceedings(Dixon21-clausal-overview,
 author       = {Clare Dixon},
 year         = {2021},
 title        = {Theorem Proving Using Clausal Resolution: From Past to Present},
 editor       = {Paul C. Bell and Patrick Totzke and Igor Potapov},
 booktitle    = {Reachability Problems - 15th International Conference, {RP} 2021, Liverpool, UK, October 25-27, 2021, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {13035},
 publisher    = {Springer},
 pages        = {19--27},
 doi          = {10.1007/978-3-030-89716-1\_2},
)
@article(DixonBF05,
 author       = {Clare Dixon and Alexander Bolotov and Michael Fisher},
 year         = {2005},
 title        = {Alternating Automata and Temporal Logic Normal Forms},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {135},
 number       = {1-3},
 pages        = {263--285},
 doi          = {10.1016/j.apal.2005.03.002},
)
@incollection(Emerson90,
 author       = {E. Allen Emerson},
 year         = {1990},
 title        = {{T}emporal and {M}odal {L}ogic},
 editor       = {Jan van Leeuwen},
 booktitle    = {Handbook of Theoretical Computer Science: Volume B, Formal Models and Semantics},
 publisher    = {Elsevier},
 pages        = {996--1072.},
)
@article(EH85,
 author       = {E. Allen Emerson and Joseph Y. Halpern},
 year         = {1985},
 title        = {Decision procedures and expressiveness in the temporal logic of branching time},
 journal      = {Journal of Computer and System Sciences},
 volume       = {30(1)},
 pages        = {1--24},
 doi          = {10.1016/0022-0000(85)90001-7Get},
)
@article(Emerson86,
 author       = {E. Allen Emerson and Joseph Y. Halpern},
 year         = {1986},
 title        = {``Sometimes'' and ``Not Never'' Revisited: On Branching versus Linear Time Temporal Logic},
 journal      = {Journal of ACM},
 volume       = {33},
 number       = {1},
 pages        = {151\IeC{\textendash}178},
 doi          = {10.1145/4904.4999},
)
@inproceedings(ES84,
 author       = {E. Allen Emerson and A. Prasad Sistla},
 year         = {1984},
 title        = {Deciding Branching Time Logic},
 booktitle    = {Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing},
 series       = {STOC '84},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {14\IeC{\textendash}24},
 doi          = {10.1145/800057.808661},
)
@article(FL79,
 author       = {Michael J. Fischer and Richard E. Ladner},
 year         = {1979},
 title        = {Propositional dynamic logic of regular programs},
 journal      = {Journal of Computer and System Sciences},
 volume       = {18},
 number       = {2},
 pages        = {194--211},
 doi          = {10.1016/0022-0000(79)90046-1},
)
@article(Fi97,
 author       = {Michael Fisher},
 year         = {1997},
 title        = {A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution},
 journal      = {Journal of Logic and Computation},
 volume       = {7},
 number       = {4},
 pages        = {429--456},
 doi          = {10.1093/logcom/7.4.429},
)
@article(FDP2001,
 author       = {Michael Fisher and Clare Dixon and Martin Peim},
 year         = {2001},
 title        = {Clausal Temporal Resolution},
 journal      = {{ACM} Transactions on Computational Logic},
 volume       = {2},
 number       = {1},
 pages        = {12--56},
 doi          = {10.1145/371282.371311},
)
@article(Lar-Quant-CTL-2014,
 author       = {Fran{\c{c}}ois Laroussinie and Nicolas Markey},
 year         = {2014},
 title        = {Quantified {CTL:} Expressiveness and Complexity},
 journal      = {Logical Methods in Computer Science},
 volume       = {10},
 number       = {4},
 pages        = {1--45},
 doi          = {10.2168/LMCS-10(4:17)2014},
)
@article(Fisher-2019-Verification-of-Autonomous-systems,
 author       = {Matt Luckcuck and Marie Farrell and Louise A. Dennis and Clare Dixon and Michael Fisher},
 year         = {2019},
 title        = {Formal Specification and Verification of Autonomous Robotic Systems: {A} Survey},
 journal      = {{ACM} Comput. Surv.},
 volume       = {52},
 number       = {5},
 pages        = {100:1--100:41},
 doi          = {10.1145/3342355},
)
@incollection(Vardi06automata-theoretictechniques,
 author       = {Moshe Y. Vardi},
 year         = {2007},
 title        = {Automata-theoretic Techniques for Temporal Reasoning},
 editor       = {Patrick Blackburn and Johan F. A. K. van Benthem and Frank Wolter},
 booktitle    = {Handbook of Modal Logic},
 series       = {Studies in logic and practical reasoning},
 volume       = {3},
 publisher    = {North-Holland},
 pages        = {971--989},
 doi          = {10.1016/s1570-2464(07)80020-6},
)
@inproceedings(ZhangHD09,
 author       = {Lan Zhang and Ullrich Hustadt and Clare Dixon},
 year         = {2009},
 title        = {A Refined Resolution Calculus for CTL},
 booktitle    = {CADE-22},
 pages        = {245--260},
 doi          = {10.1007/978-3-642-02959-2_20},
)
@article(ZhangHD10,
 author       = {Lan Zhang and Ullrich Hustadt and Clare Dixon},
 year         = {2010},
 title        = {{CTL-RP:} {A} computation Tree Logic Resolution Prover},
 journal      = {{AI} Commun.},
 volume       = {23},
 number       = {2-3},
 pages        = {111--136},
 doi          = {10.3233/AIC-2010-0463},
)