References

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