The homepage of Lucas Dixon...
"Self-importance is the nemesis of mankind." - Juan.
reasoning over compact closed categories, with applications to quantum
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.
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
Network), semantics of quantum computation
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.
- The Theory behind TheoryMine. A. Bundy,
R. McCasland. [draft 2011-02-28, pdf]
- A Calculus for Conjecture Synthesis. M. Johansson, L. Dixon and A. Bundy. [draft 2011-01-31, pdf]
- Open Graphs and Monoidal Theories. L. Dixon, A. Kissinger [31
pages, Draft of Nov 2010, pdf]
- Scheme-based Theorem Discovery and Concept Invention. O. Montano-Rivas, R. McCasland, L. Dixon, A. Bundy [40
pages, Draft of Nov 2010, pdf]
- Open Rationalism; Scotland, my utopia. L. Dixon [2
pages, Draft of Jan 2009, pdf]
My favorite of my publications:
- Open Graphs and Computational Reasoning. L. Dixon,
R. Duncan, A. Kissinger.
DCM 2010, EPTCS,
[12 pages, pdf]
- Conjecture Synthesis for Inductive
Theories. M. Johansson, L. Dixon, A. Bundy. JAR 2010 [39 pages,
21 Feb 2010, 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:
- Dynamic Rippling, Middle-Out Reasoning, and Lemma
Discovery. M. Johansson, L. Dixon, A. Bundy. Walther Festschrift, LNAI 6463, Springer. [16
- Case-Analysis for Rippling and Inductive
Proof. M. Johansson, L. Dixon, A. Bundy. ITP 2010, LNCS 6172, Springer. [16 pages, 22 Jan
- Basic Elements of Logical Graphs. L. Dixon. Workshop on Computer Algebra Methods and Commutativity of Algebraic Diagrams. [Extended abstract, 13 pages,
- Monoidal Categories, Graphical Reasoning, and Quantum Computation. Workshop on Computer Algebra Methods and Commutativity of Algebraic Diagrams. [Extended abstract, 14 pages,
- 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,
- 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:
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,
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
[slides as pdf, 1hr
with demo] Invited talk
Wednesday Seminar, University of Cambridge, 27 Jan 2010.
- Graphical Calculi for Reasoning about Quantum Information
[slides as pdf, 20min] talk
grant advisory panel 2009, University of Edinburgh, 11 Dec
- Graphical Logic and Logical Graphs
[slides as pdf, 40min]
Centenary Symposium, University of St. Andrews, 24 Nov 2009.
- Graphical reasoning in symmetric monoidal categories
as pdf, 1h] Invited talk
at Logic and
Graph Transformation Workshop, University of Leicester, 5 Nov
- Plans, Actions and Dialogues using Linear Logic
[slides as pdf, 1h] ICCS
Seminar, University of Edinburgh, 13 Dec 2007.