@INPROCEEDINGS{2003:Dixon:CADE, author = {L. Dixon and J. D. Fleuriot}, title = {Isa{P}lanner: A Prototype Proof Planner in {I}sabelle}, booktitle = {Proceedings of {CADE}'03}, year = {2003}, volume = {2741}, series = {LNCS}, pages = {279--283}, key = {Dixon}, } @INPROCEEDINGS{2004:Dixon:TPHOLs, author = {L. Dixon and J. D. Fleuriot}, title = {Higher Order Rippling in {IsaPlanner}}, booktitle = {Theorem Proving in Higher Order Logics}, year = {2004}, volume = {3223}, series = {LNCS}, pages = {83--98}, key = {Dixon}, } @INPROCEEDINGS{2005:Bundy:CLASE, author = {A. Bundy and L. Dixon and J. Gow and J. Fleuriot}, title = {Constructing induction rules for deductive synthesis proofs}, booktitle = {ETAPS-05: Workshop on Constructive Logic for Automated Software Engineering (CLASE-05)}, year = {2006}, pages = {3--21}, volume = 153, issue = 1, publisher = {ENTCS}, key = {Bundy}, } @ARTICLE{2005:Dixon:JAL, author = {L. Dixon and J. D. Fleuriot}, title = {A Proof-Centric approach to Mathematical Assistants}, journal = {Journal of Applied Logic: Towards Computer Aided Mathematics Systems}, pages = {505--532}, year = {2005}, volume = {4}, number = {4}, key = {Dixon}, url = {http://www.sciencedirect.com/science/article/B758H-4HKD001-3/2/1edf4841d8a8d15ca423b0a1ffc1431f} } @PHDTHESIS{2005:Dixon:Phd, author = {L. Dixon}, title = {A Proof Planning Framework for {Isabelle}}, school = {University of Edinburgh}, year = {2005}, } @INPROCEEDINGS{2005:Dixon:UITP, author = {L. Dixon}, title = {Interactive and Hierarchical Tracing of Techniques in IsaPlanner}, booktitle = {Proceedings of the ETAPS-05 Workshop on User Interfaces for Theorem Provers (UITP-05), Edinburgh}, year = {2005}, editor = {D. Aspinall}, pages = {13}, publisher = {LFCS University of Edinburgh}, note = {Published in ENTCS.}, key = {Dixon}, } @inproceedings{2006:Johansson:Aiello, author = {M. Johansson and A. Bundy and L. Dixon}, title = {Best-First Rippling}, booktitle = {Reasoning, Action and Interaction in AI Theories and Systems, Essays Dedicated to Luigia Carlucci Aiello}, year = {2006}, pages = {83-100}, publisher = {Springer}, editor = {Oliviero Stock and Marco Schaerf}, series = {Lecture Notes in Computer Science}, volume = {4155}, year = {2006}, ee = {http://dx.doi.org/10.1007/11829263_5}, bibsource = {DBLP, http://dblp.uni-trier.de}, note = {An extended version is available as University of Edinburgh Technical Report EDI-INF-RR-0849, http://www.inf.ed.ac.uk/} } @INPROCEEDINGS{2008:DixonDuncan:AISC, author = {L. Dixon and R. Duncan}, title = {Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation}, booktitle = {Proceedings of {AISC}'08}, year = {2008}, series = {LNAI}, publisher = {Springer} } @INPROCEEDINGS{2009:Dixon:VVPS, author = {L. Dixon and A. Smaill and A. Bundy}, title = {Verified Planning by Deductive Synthesis in Intuitionistic Linear Logic}, booktitle = {Proceedings of {VVPS}'09}, year = {2009}, pages = {10}, key = {Dixon}, } @ARTICLE{2009:DixonDuncan:AMAI, author = {L. Dixon and R. Duncan}, title = {Graphical Reasoning in Compact Closed Categories for Quantum Computation}, journal = {AMAI}, volume = {56}, number = {1}, pages = {20}, publisher = {Springer}, year = {2009}, url = {http://www.springerlink.com/content/101739/?Content+Status=Accepted} } @ARTICLE{2009:DixonSmaillTsang:JLLI, author = {L. Dixon and A. Smaill and T. Tsang}, title = {Plans, Actions and Dialogue using Linear Logic}, journal = {Journal of Logic, Language and Information}, pages = {48}, number = {2}, volume = {18}, publisher = {Springer}, year = {2009}, url = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s10849-008-9079-0} } @INPROCEEDINGS{2010:DDK:DCM, author = {L. Dixon and R. Duncan and A. Kissinger}, title = {Open Graphs and Computational Reasoning}, booktitle = {Proceedings of {DCM}'10}, volume = {26}, publisher = {EPTCS}, year = {2010}, pages = {169-180}, } @incollection {2010:JDB:ITP, author = {M. Johansson and L. Dixon and A. Bundy}, title = {Case-Analysis for Rippling and Inductive Proof}, booktitle = {Interactive Theorem Proving}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {}, pages = {291-306}, volume = {6172}, url = {http://dx.doi.org/10.1007/978-3-642-14052-5_21}, year = {2010} }