lucas dixon

I am Lucas Dixon, and I was 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. I was 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.

I now work for Google in New York and have a double-life as a visting research scientist in Edinburgh, so you can still contact me by email on the above address.

"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.
TheoryMine: A novelty gift company selling exciting new pieces of mathematics.
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.
QUISCO: Quantum Information Science Scotland.
Co-organiser of the CISA seminars at the University of Edinburgh.
Previous Events I organised or helped with.

(bibtex)

Drafts:

Open Rationalism; Scotland, my utopia. L. Dixon [2 pages, Draft of Jan 2009, pdf]

My favorite of my publications:

Open Graphs and Monoidal Theories. L. Dixon, A. Kissinger [31 pages, Journal of MSCS 2012 preprint pdf]
The Theory behind TheoryMine. A. Bundy, F. Cavallo, L. Dixon, M. Johansson, R. McCasland. [draft 2012-03-29, accepted for IFColog special issue on Automatheo, preprint pdf]
Conjecture Synthesis for Inductive Theories. M. Johansson, L. Dixon, A. Bundy. JAR 2010 [39 pages, 21 Feb 2010, preprint pdf]
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:

Scheme-based Theorem Discovery and Concept Invention. O. Montano-Rivas, R. McCasland, L. Dixon, A. Bundy [40 pages, ACM link, Journal of ESW 2011, preprint pdf]
Open Graphs and Computational Reasoning. L. Dixon, R. Duncan, A. Kissinger. DCM 2010, EPTCS, [12 pages, pdf]
A Calculus for Conjecture Synthesis. M. Johansson, L. Dixon and A. Bundy. [draft 2011-01-31, accepted for IFColog special issue on Automatheo, pdf]
Dynamic Rippling, Middle-Out Reasoning, and Lemma Discovery. M. Johansson, L. Dixon, A. Bundy. Walther Festschrift, LNAI 6463, Springer. [16 pages, 2010, pdf]
Case-Analysis for Rippling and Inductive Proof. M. Johansson, L. Dixon, A. Bundy. ITP 2010, LNCS 6172, Springer. [16 pages, 22 Jan 2010, pdf]
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 Reasoning in Symmetric Monoidal Categories for Quantum Information [slides as pdf, 1hr with demo] Invited talk for The Wednesday Seminar, University of Cambridge, 27 Jan 2010.
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.

Atheist Advent - Twenty- four solstice songs, played on a godless guitar.
my travel blog
Mateo
Lucy
Graham Steel
Ricardo, Su, and other's Tango Blog

lucas dixon

thoughts

research/projects

organisational

publications

a few of my later scientific talks

likes

links

blogs