Clare Dixon - Publications

Journal Articles

• Konur S., Dixon C., and Fisher M.
  Analysing Robot Swarm Behaviour via Probabilistic Model Checking
  Robotics and Autonomous Systems, Elsevier, 2011

• Zhang L., Hustadt U. and Dixon C.
  CTL-RP: A Computation Tree Logic Resolution Prover.
  AI Communications, 23(2-3):111-136, IOS Press, 2010.

• Behdenna A., Dixon C. and Fisher M.
  Deductive Verification of Simple Foraging Robotic Behaviours.
  International Journal of Intelligent Computing and Cybernetics, 2(4): 604-643, World Scientific, 2009

• Nalon, C., and Dixon, C.
  Clausal Resolution for Normal Modal Logics
  Journal of Algorithms, Volume 62, Issues 3-4, July-October 2007, Pages 117-134 Elsevier Science, 2007

• Dixon, C., Fernandez Gago, M.C., Fisher, M., and van der Hoek, W.,
  Temporal Logics of Knowledge and their Applications in Security
  Proceedings of the First Workshop in Information and Computer Security (ICS 2006) Timisoara, Romania, Edited by C. Dima, M. Minea and F.L. Tiplea, Electronic Notes in Theoretical Computer Science, Volume 186, Pages 27-42 (July 2007) Elsevier, 2007.

• Dixon, C.,
  Using Temporal Logics of Knowledge for Specification and Verification-a Case Study
  Journal of Applied Logic, Elsevier Science, 4(1) pages 50-78, 2006.

• Fernandez-Gago, M.C., Hustadt, U., Dixon, C., Fisher, M., and Konev, B.,
  First-Order Temporal Verification in Practice,
  Journal of Automated Reasoning, 34(3) pages 295-321, Kluwer, 2005.

• Winfield, A.F.T., Sa, J., Fernandez-Gago, M-C., Dixon, C., and Fisher, M.
  On Formal Specification of Emergent Behaviours in Swarm Robotic Systems
  International Journal Of Advanced Robotic Systems, 2(4), pages 363-370, 2005

• Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.,
  Mechanizing First-Order Temporal Resolution
  Information and Computation, 199(1-2), pages 55-86. Elsevier Science, 2005.

• Dixon, C., Bolotov, A., and Fisher, M.,
  Alternating Automata and Temporal Logic Normal Forms
  Annals of Pure and Applied Logic, 135(1-3), pages 263-285. Elsevier Science, September 2005.

• Dixon, C., Nalon, C. and Fisher, M.,
  Tableau for Logics of Time and Knowledge with Interactions Relating to Synchrony,
  Journal of Applied Non-Classical Logics, volume 14, number 4, pages 397-445, 2004.
  

• Dixon, C., Fisher, M., and Bolotov, A.
  Clausal Resolution in a Logic of Rational Agency
  in Artificial Intelligence Journal, volume 139, issue 1, July 2002 pages 47-89. Elsevier Science.
  

• Bolotov, A., Fisher, M., and Dixon, C.
  On the Relationship Between Omega-Automata and Temporal Logic Normal Forms
  in the Journal of Logic and Computation, volume 12, issue 4, pages 561-581, August 2002. Oxford University Press.
  (Preliminary version.)

• Bennett, B., Dixon, C., Fisher M., Hustadt, U., Franconi, E., Horrocks, I., de Rijke, M.
  Combinations of Modal Logics,
  AI Review, volume 17, number 1, pages 1-20, March 2002. Kluwer Academic Publishers.
  (Preliminary version.)

• Fisher, M., Dixon, C., and Peim, M.
  Clausal Temporal Resolution,
  ACM Transactions on Computational Logic, volume 2, number 1, January 2001

• Dixon, C.,
  Removing Irrelevant Information in Temporal Resolution Proofs,
  in the Journal of Experimental and Theoretical Artificial Intelligence, volume 11, pages 95-121, 1999. ISSN 0952-813X.
  (Preliminary version.)

• Dixon, C., Fisher, M., and Wooldridge, M.,
  Resolution for Temporal Logics of Knowledge,
  in the Journal of Logic and Computation, volume 8, number 3, 1998. ISSN 0955-792X.
  (Preliminary version.)

• Wooldridge, M., Dixon, C., and Fisher, M.,
  A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief ,
  in the Journal of Applied Non-Classical Logics, volume 8, number 3, 1998. ISSN 1166-3081.
  (Preliminary version.)

• Dixon, C.,
  Temporal Resolution using a Breadth-First Search Algorithm,
  in the Annals of Mathematics and Artificial Intelligence, volume 22, pages 87--115,
  special issue on Temporal Representation and Reasoning 1998. Baltzer Science Publishers. ISSN 1012-2443.
  (Preliminary version.)

Book Chapters

• Hustadt, U., Dixon, C., Schmidt, R.A., Fisher, M., Meyer, J.-J., van der Hoek, W.,
  Verification Within the KARO Agent Theory
  In Agent Technology from a Formal Perspective. Springer-Verlag, 2006.
  

• Reynolds, M., and Dixon, C.
  Theorem-Proving for Discrete Temporal Logic,
  to appear in the Handbook of Temporal Reasoning in Artificial Intelligence, 1, Foundations of Artificial Intelligence Series, Elsevier, 2005

Articles in Conference or Workshop Proceedings

• Dixon, C., Winfield , A.F.T., and Fisher, M.,
  Towards Temporal Verification of Emergent Behaviours in Swarm Robotic Systems.
  in the Proceedings of the 12th Conference Towards Autonomous Robotic Systems. 31st August - 2nd September 2011, Sheffield, UK. LNCS, Springer
  

• Stocker, R., Sierhuis, M., Dennis, L., Dixon C., and Fisher M.,
  A Formal Semantics for Brahams.
  in the Proceedings of the 12th International Workshop on Computational Logic in Multi-Agent Systems. 17th-18th July 2011, Barcelona, Spain. LNCS, Springer.
  

• McCabe-Dansted, J. and Dixon, C.,
  CTL-Like Fragments of a Temporal Logic of Robustness
  in the Proceedings of TIME 2010, 6th-8th September 2010, Paris, France. IEEE Press.
  

• Konur S, Dixon C, and Fisher M,
  Formal Verification of Probabilistic Swarm Behaviours
  in the Proceedings of the Seventh International Conference on Swarm Intelligence (ANTS2010), 8-10th September 2010, Brussels, Belgium. LNCS, Springer.

• Dixon C, Fisher M and Konev B,
  Taming the Complexity of Temporal Epistemic Reasoning.
  In: Ghilardi S and Sebastiani R ed(s) Proceeding of the Seventh International Symposium on the Frontiers of Combining Systems (FRoCoS'09). 16-18th September, Trento, Italy. LNAI, Springer 2009

• Konev B, Dixon C, and Fisher M,
  Playing Cards with Wiebe [Solving Knowledge Puzzles with "Exactly One" S5n]
  In: Proceeding of the Wiebefest 2009 16th March 2009, Liverpool, UK

• Zhang, L., Hustadt, U., and Dixon, C.,
  A Refined Resolution Calculus for CTL
  In Proceedings of 22nd International Conference on Automated Deduction (CADE-22) McGill University, Montreal, Canada August 2 - 7, 2009. Springer LNCS/LNAI
  

• Dixon, C., Fisher, M., Konev, B., and Lisitsa, A.,
  Practical First-Order Temporal Reasoning
  in the Proceedings of TIME 2008, 16th-18th June 2008, Montreal, Canada. IEEE Press.
  

• Dixon, C., Fisher, M., and Konev, B.,
  Temporal Logic with Capacity Constraints
  in the Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS), September 10-12, Liverpool, UK. LNAI, Springer 2007.

• Dixon, C., Fisher, M., and Konev, B.,
  Tractable Temporal Reasoning
  in the Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07), pages 318-323, January 6-12th 2007, Hyderabad, India

• Nalon, C., and Dixon, C.
  Normal Modal Resolution: Preliminary Results,
  to appear in the Proceedings of the Brazilian Workshop on Logical and Semantic Frameworks, with Applications (LSFA'06) September 17th 2006, Natal, Brazil

• Nalon, C., and Dixon, C.
  Anti-Prenexing and Prenexing for Modal Logics,
  in the Proceedings of JELIA 06, 13-15th September, Liverpool, UK. LNAI, Springer 2006.

• Dixon, C., Fisher, M., and Konev, B.,
  Is There a Future for Deductive Temporal Verification?
  in the Proceedings of TIME 2006, 15th-17th June 2006, Budapest, Hungary IEEE.
  The extended version is published as University of Liverpool Technical Report number ULMS-06-01

• Winfield, A.F.T., Sa, J., Fernandez-Gago, M-C., Dixon, C., and Fisher, M.
  Using Temporal Logic to Specify Emergent Behaviours in Swarm Robotic Systems
  In Towards Autonomous Robotic Systems (TAROS), 2005

• Nalon, C., Dixon, C. and Fisher, M.
  Resolution for Synchrony and No Learning,
  in the Proceedings of AiML-5, Manchester, UK. Advances in Modal Logic Series, Kings College Publications, volume 5, pages 231-248, 2005. Editors Renate Schmidt,Ian Pratt-Hartmann, Mark Reynolds, and Heinrich Wansing. (Extended version of the paper below).

• Nalon, C., Dixon, C. and Fisher, M.
  Resolution for Synchrony and No Learning,
  in the Preliminary Proceedings of AiML-5, 9-11th September 2004, Manchester, UK.
  Published as University of Manchester Technical Report Number UMCS-04-09-01 pages 303-317.

• Dixon, C.,
  Miss Scarlett in the Ballroom with the Lead Piping
  in Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004), Valencia, Spain 22nd-27th August 2004. IOS Press.
  Slightly extended version of that which appears in the proceedings.

• Dixon, C., Fernandez Gago, M.C., Fisher, M., and van der Hoek, W.,
  Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols
  in the Proceedings of TIME 2004, 1st-3rd July 2004, Tatihou, Normandie, France. IEEE.

• Dixon, C., Nalon, C., and Fisher, M.
  Tableaux for Temporal Logics of Knowledge: Synchronous Systems of Perfect Recall or No Learning
  in the Proceedings of TIME-ICTL 2003, July 8-10 July 2003, Cairns, Queensland, Australia. IEEE.
  Slides (PDF, postscript)

• Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.,
  Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case
  in the Proceedings of TIME-ICTL 2003, July 8-10 July 2003, Cairns, Queensland, Australia. IEEE.
  Slides (PDF, postscript)

• Fernandez Gago, M.C., Fisher, M., and Dixon C.,
  Algorithms for Guiding Clausal Temporal Resolution
  in the 25th Conference on Artificial Intelligence (KI2002) September 16-20, 2002, pp 235--249, Aachen, Germany. LNAI, volume 2479, Springer 2002.

• Fernandez Gago, M.C., Fisher, M., and Dixon C.,
  An Algorithm for Guiding Clausal Temporal Resolution,
  in Proceedings of 4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001), held in conjunction with IJCAR 2001, June 18th 2001, Siena, Italy.

• Nalon, C., Dixon, C. and Fisher, M.
  Resolution for Synchrony and No Learning: Preliminary Report,
  in Proceedings of the 8th International Workshop on Logic Language, Information and Computation (WoLLIC'2001).

• Hustadt, U., Dixon, C., Schmidt, R.A., Fisher, M., Meyer, J.-J., and van der Hoek, W.,
  Reasoning about agents in the KARO framework,
  in the Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME-01),IEEE Computer Society Press, pp 206-213. June 14-16, 2001, Cividale del Friuli, Italy.

• Dixon, C., and Fisher, M.,
  Clausal Resolution for Logics of Time and Knowledge with Synchrony and Perfect Recall,
  in Proceedings of ICTL 2000, 4th-7th October 2000, pp 43-52, Leipzig, Germany.

• Bolotov, A., Fisher, M., and Dixon, C.,
  On the Relationship between w-Automata and Temporal Logic Normal Forms,
  in Proceedings of ICTL 2000, 4th-7th October 2000, Leipzig, Germany. (Extended version.)

• Dixon, C., Fisher, M., and Bolotov, A.
  Resolution in a Logic of Rational Agency,
  in Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000), Berlin, Germany 23rd-25th August 2000. IOS Press.

• Dixon, C. and Fisher, M.
  Resolution-Based Proof for Multi-Modal Temporal Logics of Knowledge ,
  in Proceedings of the Seventh International Workshop on Temporal Representation and Reasoning (TIME'00), S Goodwin and A Trudel (eds) IEEE Computer Society pp 69-78.ISBN 0-7695-0756-5 Cape Breton, Nova Scotia, Canada, July 7-9, 2000.

• Bolotov, A. and Dixon, C.,
  Resolution for Branching-Time Temporal Logics: Applying the Temporal Resolution Rule,
  in Proceedings of the Seventh International Workshop on Temporal Representation and Reasoning (TIME'00), S Goodwin and A Trudel (eds) IEEE Computer Society pp 163-172.ISBN 0-7695-0756-5, Cape Breton, Nova Scotia, Canada, July 7-9, 2000.

• Hustadt, U., Dixon, C., Schmidt, R.A., Fisher, M., Meyer J.-J. and van der Hoek, W.
  Verification within the KARO Agent Theory,
  in Proceedings of the first Goddard Workshop on Formal Approaches to Agent-Based Systems (FAABS), Goddard Space Flight Center, Greenbelt, Maryland, USA, 5th-7th April 2000. LNCS 1871, Springer 2001.

• Hustadt, U., Dixon, C., Schmidt, R.A., and Fisher, M.,
  Normal Forms and Proofs in Combined Modal and Temporal Logics ,
  in the Proceedings of the Third International Workshop on the Frontiers of Combining Systems (FroCoS'2000), Nancy, France. March 22-24, 2000. LNAI, Springer.

• Bolotov, A., Dixon, C., and Fisher, M.,
  Clausal Resolution for CTL* ,
  in the Proceedings of the 24th International Symposium on Mathematical Foundations of Computer Science, September 6-10, 1999, Szklarska Poreba, Poland. LNCS, volume 1672, pages 137-148, Springer.

• Dixon, C. and Fisher M.,
  The Set of Support Strategy in Temporal Resolution,
  in Proceedings of the Fifth International Workshop on Temporal Reasoning (TIME'98), pages 113-120, Sanibel Island, Florida, May 1998. IEEE Press. ISBN0-8186-8473-9. Please note the IEEE copyright.

• Dixon, C. and Fisher, M.,
  Tableaux for Synchronous Systems of Knowledge and Time with Interactions,
  in Proceedings of the Sixth Scandinavian Conference on Artificial Intelligence (SCAI'97), pages 28-39 Helsinki, Finland August 1997. IOS Press. ISBN 90 5199 354 4

• Dixon, C.,
  Using Otter for Temporal Resolution,
  in Proceedings of the Second International Conference on Temporal Logic (ICTL'97), Manchester, UK, July 1997. In Advances in Temporal Logic, volume 16, pages 149--166, 2000. Kluwer. ISBN 0-7923-6149-0 (Pre-proceedings version)

• Dixon, C., Fisher, M., and Reynolds, M.,
  Execution and Proof in Horn-Clause Temporal Logic,
  in Proceedings of the Second International Conference on Temporal Logic (ICTL'97), Manchester, UK, July 1997. In Advances in Temporal Logic, volume 16, pages 413--434, 2000. Kluwer. ISBN 0-7923-6149-0. (Pre-proceedings version)

• Fisher, M., and Dixon, C.,
  Guiding Clausal Temporal Resolution,
  in Proceedings of the Second International Conference on Temporal Logic (ICTL'97), Manchester, UK, July 1997. In Advances in Temporal Logic, volume 16, pages 167--184, 2000. Kluwer. ISBN 0-7923-6149-0 (Pre-proceedings version)

• Dixon, C.,
  Temporal Resolution: Removing Irrelevant Information,
  in Proceedings of the Fourth International Workshop on Temporal Reasoning (TIME'97), Daytona Beach, Florida, May 1997. IEEE Press. Please note the IEEE copyright.

• Dixon, C.,
  Search Strategies for Resolution in Temporal Logics,
  in the International Conference on Automated Deduction (CADE-13), New Jersey, USA July, August 1996. Springer.

• Fisher, M., Wooldridge, M., and Dixon, C.,
  A Resolution-Based Proof Method for Temporal Logics of Knowledge and Belief,
  in the International Conference on Formal and Applied Practical Reasoning (FAPR-96), Bonn, Germany June 1996.

• Dixon, C.,
  Temporal Resolution: A Breadth-First Search Approach,
  in Proceedings of the Third International Workshop on Temporal Reasoning (TIME'96), Key West, Florida, May 1996. IEEE Press. Please note the IEEE copyright.

• Dixon, C., Fisher, M., and Johnson, R.,
  Parallel Temporal Resolution,
  in Proceedings of International Workshop on Temporal Reasoning (TIME'95), Melbourne Beach, Florida, April 1995.

• Dixon, C., Fisher, M., and Barringer, H.,
  A Graph-Based Approach To Resolution In Temporal Logic,
  in First International Conference on Temporal Logic (ICTL), held in Bonn, Germany, July 1994. Springer.

Technical Reports

• Nalon, C., and Dixon, C.
  Anti-Prenexing and Prenexing for Modal Logics (Extended Version)
  University of Liverpool Technical Report number ULMS-06-003
  (Extended version of JELIA06 paper.)

• Dixon, C., Fisher, M., and Konev, B.,
  Is There a Future for Deductive Temporal Verification?
  University of Liverpool Technical Report number ULMS-06-001
  (Extended version of TIME06 paper.)

• Dixon, C.
  Specifying and Verifying the Game Cluedo using Temporal Logics of Knowledge
  University of Liverpool Technical Report number ULCS-04-003

• Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U.,
  Mechanising First-Order Temporal Resolution
  University of Liverpool Technical Report number ULCS-03-023

• Dixon, C., Fernandez Gago, M.-C., Fisher M., and van der Hoek, W.,
  Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols
  University of Liverpool Technical Report number ULCS-03-022

• Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U.
  Towards the Implementation of First-Order Temporal Resolution: The Expanding Domain Case.
  University of Liverpool Technical Report number ULCS-03-005

• Dixon, C.,
  Strategies for Temporal Resolution,
  PhD thesis, The University of Manchester, September 1995. Also Technical Report number UMCS-95-12-1, ISSN 1361-6153, Department of Computer Science, University of Manchester, December 1995. (It's a large file so be warned!)

• Dixon, C.,
  A Graph-Based Approach to Resolution in Temporal Logic,
  Technical Report number UMCS-93-9-2, Department of Computer Science, University of Manchester, September 1993.

Edited Books/Journals/Conference Proceedings

• Artale, A., Dixon,C., Fisher, M. and Franconi, E., (editors)
  Special Issue on Temporal Representation and Reasoning (TIME),
  Journal of Logic and Computation, volume 14, number 1, 2004. Oxford University Press. ISSN 0955-792X.

• Dixon,C., Finger, M., Fisher, M. and Reynolds, M., (editors)
  Special Issue on Temporal Representation and Reasoning,
  Annals of Mathematics and Artificial Intelligence, volume 30, numbers 1-4, 2001. Kluwer. ISSN 1012-2443.

• Dixon, C. and Fisher, M., (editors)
  Proceedings of the Sixth International Workshop on Temporal Representation and Reasoning (TIME-99),
  Orlando, Florida, May 1999. IEEE Press, ISBN 0-7695-0173-7.