lucas dixon

I am Lucas Dixon, a researcher with the mathematical reasoning group, part of the centre for intelligent systems and their applications, in the school of informatics, at the University of Edinburgh. Currently funded by EPSRC Platform grant EPE/005713/1 "The Integration and Interaction of Multiple Mathematical Reasoning Processes". From 1 Apr 2007 - 31 March 2011.

You can contact me by email at: lucas dot dixon at ed.ac.uk, telephone: +44 (0) 131 651 3260, fax: +44 (0)131 650 6899, or post/visit me: Rm.2.02, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB, UK.

"Self-importance is the nemesis of mankind." - Juan.

other thoughts...

Quantomatic: reasoning over compact closed categories, with applications to quantum information processing.
Dialogue Planning with Linear Logic: using intuitionistic linear logic to allow distributed asyncronous systems to interact in a robust way, and prove properties about such interactions.
PolyML Interface: I have been working on PolyML with David Matthews to provide a PolyML IDE-style interface, based on jEdit, for writing Standard ML code.
IsaPlanner: a framework for proof planning in Isabelle. The idea's behind IsaPlanner are described in my thesis.
ken yersel is a project aiming to provide an educative, democratic, transparent, form of particpatory discussion. It combines dialectic democracy and argument mapping for more rational, but still scalable, informed decision making. Recently working on building implementation which will live at: http://www.thoughtvine.org
Teaching and Project supervision
A few old programming projects
More generally, my research interests include democratic participation, dialogue - both in practice and in thoery as well as creative and argumentative, type theory (TYPES Network), semantics of quantum computation (QNET Network), game theory, category theory, graph theory, number theory, inductive theorem proving, first-order and higher-order theorem proving, algorithm complexity, computer algebra, interfaces for theorem proving, functional and logic programming languages, linear logic, and lots of other stuff.

Programme co-chair of PLMMS 2010 co-located with CICM 2010.
Programme co-chair of Automatheo 2010 workshop at FLoC 2010.
Programme and organisational committe of DCM 2010 at FLoC 2010.
Co-chair of SSFRR 2010 (Summer School in Formal Representation and Reasoning) co-located with VSTTE 2010.
Programme committe of Calculemus 2010, and AISC 2010.
Co-organiser of the CISA seminars at the University of Edinburgh.
Previous Events I organised or helped with.

Drafts:

Lemma Discovery and Middle-Out Reasoning for Automated Inductive Proofs. M. Johansson, L. Dixon, A. Bundy. [16 pages, Draft: 22 Jan 2010, pdf]
Case-Analysis for Rippling and Inductive Proof. M. Johansson, L. Dixon, A. Bundy. [16 pages, Draft: 22 Jan 2010, pdf]
Conjecture Synthesis for Inductive Theories. M. Johansson, L. Dixon, A. Bundy. [42 pages, Draft: 3 Nov 2009, pdf]
Open Rationalism; Scotland, my utopia. L. Dixon [2 pages, Draft of Jan 2009, pdf]

Main Publications: (bibtex)

Graphical Reasoning in Compact Closed Categories for Quantum Computation. L. Dixon and R. Duncan. Annals of Mathematics and Artificial Intelligence: Volume 56, Issue 1 (2009) [22 pages, 2009, pdf, Inf.Rep.1301, Springer]
Plans, Actions and Dialogue using Linear Logic. L. Dixon, A. Smaill, T. Tsang, in the Journal of Logic, Language and Information [48 pages, JoLLI 2009, pdf, Inf.Rep.1300]
A Proof-Centric approach to Mathematical Assistants. L. Dixon and J. D. Fleuriot. Journal of Applied Logic, available from ScienceDirect in Special Issue on Mathematics Assistance Systems. [35 pages, 2005, pdf]

Other Selected Publications:

Basic Elements of Logical Graphs. L. Dixon. Workshop on Computer Algebra Methods and Commutativity of Algebraic Diagrams. [Extended abstract, 13 pages, 2009, pdf]
Monoidal Categories, Graphical Reasoning, and Quantum Computation. Workshop on Computer Algebra Methods and Commutativity of Algebraic Diagrams. [Extended abstract, 14 pages, 2009, pdf]
Verified Planning by Deductive Synthesis in Intuitionistic Linear Logic. L. Dixon, A. Smaill, A. Bundy. Verification and Validation of Planning and Scheduling Systems. [10 pages, 2009, pdf]
Reflecting Data: Formally Correct Results for Efficient (and Dirty) Algorithms. L. Dixon. Calculemus Emerging Trends [7 pages, 2009, pdf]
IsaPlanner 2: A Proof Planner in Isabelle. L. Dixon and M. Johansson. Informatics Technical Report 1302 [5 pages, 2007, pdf]
Best-First Rippling. M. Johansson, A. Bundy and L. Dixon. Strategies in Automated Deduction, part of IJCAR'06. [16 pages, 2006, pdf]
A Proof Planning Framework for Isabelle. L. Dixon. PhD Thesis, Informatics, University of Edinburgh. [225 pages, 2005, pdf]
Constructing Induction Rules for Deductive Synthesis Proofs. A. Bundy, L. Dixon, J. Gow, J. D. Fleuriot. In ENTCS: Constructive Logic for Automated Software Engineering'05. [18 pages, 2005, pdf]
Interactive and Hierarchical Tracing of Techniques in IsaPlanner. L. Dixon. ENTCS: User Interfaces for Theorem Provers'05. [13 pages, 2005, pdf].
Higher Order Rippling in IsaPlanner. L. Dixon and J. D. Fleuriot. Theorem Proving in Higher Order Logics'04, (Springer LNCS Volume 3223, 2004). [16 pages, 2004, pdf]
IsaPlanner: A Prototype Proof Planner in Isabelle. L. Dixon and J. D. Fleuriot. 19th International Conference on Automated Deduction (CADE'2003), (Springer LNCS Volume 2741, 2003). [5 pages, 2003, pdf]

Graphical Calculi for Reasoning about Quantum Information [slides as pdf, 20min] talk for platform grant advisory panel 2009, University of Edinburgh, 11 Dec 2009.
Graphical Logic and Logical Graphs [slides as pdf, 40min] Invited talk at Gentzen Centenary Symposium, University of St. Andrews, 24 Nov 2009.
Graphical reasoning in symmetric monoidal categories [slides as pdf, 1h] Invited talk at Logic and Graph Transformation Workshop, University of Leicester, 5 Nov 2009.
Plans, Actions and Dialogues using Linear Logic [slides as pdf, 1h] ICCS Seminar, University of Edinburgh, 13 Dec 2007.

Writing and reading poetry.
Mathematics - especially unsolved problems and good questions.
Art and Film - I particularly like the film Atanarjuat the fast runner and also the original version of The Ring.
I also (not so) recently saw the Japaneese cartoon Spirited Away, which I thought was a fantastic and beautiful.
Philosophy.
Dancing tango. The Edinburgh Tango Society lists all tango in Edinburgh; Rumbos de Tango - Jenni and Ricardo, a couple of the most beautiful and simpatico tango teachers and dancers (in Edinburgh!); Edinburgh University Tango; La Otra Milonga sometimes we have outdoor milongas, we usually have crazy music.
Music (Especially latin rhythms and jazzy things). Some of my friends play music I like: Ewen Maclean plays jazz (with a latin groove), I used to organise some gigs for the Big Hand, and some of my best friends in London play in the deBretts. Recently I've also been listening to Joanna Newsom, Electolane, and the Dresden Dolls.

Games.
Experimenting with dreaming, one interesting example is lucid dreaming.
Aikido and Tai Chi and more Aikido in Edinburgh.
Tickly questions.

Filmhouse, Cameo - for films in Edinburgh.
In possession of a love for games, photos and curry: Ross Duncan
Adventures with books... www.BookCrossing.com
My website from many years ago is here: the elmorian site
Some pictures from Ben in spain.
Tranport Chaos in the UK
Newsmap
Médecins Sans Frontières (MSF), an international humanitarian aid organisation that provides emergency medical assistance. In my opinion this one of the most important and effectfull charities.
Amnesty International campaign for internationally recognized human rights. Also, I think, an essential organisation for making the world a better place.

lucas dixon

thoughts

research/projects

organisational

publications

talks

likes

links

blogs