Ursula Martin
Ursula Martin CBE FRSE
Room N 3.14, Mathematical Institute
Biography
Professor Ursula Martin CBE FRSE joined the University of Oxford as Professor of Computer Science in 2014, holding a joint affiliation between the Mathematical Institute and the Department of Computer Science. She holds an EPSRC Established Career Fellowship, and a Senior Research Fellowship at Wadham College. Prior to this she held a chair of Computer Science in the School of Electronic Engineering and Computer Science at Queen Mary University of London.
At Queen Mary she was VicePrincipal for Science and Engineering (20052009), and Director of the impactQM project (20092012). She served on the U K Defence Science Advisory Council, on the 2001 and 2008 UK HEFCE RAE panel for Computer Science, and was a SICSA distinguished visitor at the University of Edinburgh for 201213. Her career was interrupted by a two year period of chemotherapy and its aftermath, and she is grateful to Queen Mary for their support during this time. She has previously held appointments at the University of St Andrews (the first female professor in any discipline since its foundation in 1411), Royal Holloway University of London, Manchester and Urbana Champaign. She holds an MA in Mathematics from Cambridge, and a PhD in Mathematics from Warwick. She was appointed a Commander of the Order of the British Empire in 2012, and a Fellow of the Royal Society of Edinburgh in 2017. She is involved in many activities for women in science, and currently serves on the Royal Society's Diversity Committee.
Conferences and seminars
External presentations in 2017 include: January: AMS Joint Mathematical meetings (Ada Lovelace), University of Waterloo [open lecture] (Ada Lovelace); University of Waterloo [Faulty of Mathematics] (Future of Proof); MIT (Mathematical practice); February: University of Kent (Future of Proof); University of Leicester (Ada Lovelace); University of Oxford [Mirzakhani Society] (women in mathematics) April: University of Oxford [Faculty of Philosophy] (Future of Proof); May: University of Oxford [Faculty of English] (Ada Lovelace); University of Oxford [Mathematics Institute, open lecture] (Hidden Figures of Oxford Computing); Birkbeck London [Computer Science] (Future of Proof); June: CIE conference, Turku, Finland [keynote]; University of Glasgow, 60th anniversary of Computer SCience Department [keynote]; July: Big Proof workshop, Isaac Newton Institute, Cambridge [keynote]; ICHSTM, Rio de Janiero [history of science] (Impact of mathematics); September: UK Mathematics Trust [school students] (Ada Lovelace); Malvern Girls College and nearby schools [school students]; St Anne's Caversham and nearby schools [school students]; October: University of St Andrews Distinguished Lectures in Computer Science [open lectures]; University of Oxford [Department of Computer Science] (Social machine of mathematics); December: Enabling Mathematical Cultures Conference, Oxford [keynote].
Current research, the Social Machine of Mathematics
Since 2014 my research has been supported by an EPSRC Fellowship, investigating cultures of mathematics to understand mathematics as as a social machine. The resulting highly interdisciplinary portfolio of work, using philosophy, social scence and history alongside computer science research in artificial intelligence, argumentation theory and verification, shows the scope for new computer techniques to support concept formation and argument finding, while highlighting the roles that risk, doubt, error, explanation and group knowledge play in the human production and use of mathematics. Current postdocs are Joe Corneli, Lorenzo Lane and Fenner Tanswell: former postdocs Chris Hollings (Oxford), Gabriela Nesin (Brighton) and Alison Pease (Dundee) have moved on to lectureships.
The project will hold a workshop on "Group knowledge and mathematical collaboration" on 7 and 8 April 2017, and a workshop on "Enabling mathematical cultures" on 5, 6 and 7 December 2017
Investigation of online mathematical collaboration to understand how proof comes about, and the model provided by social machines, in particular looking at evidence from writings by mathematicians, and from study of the polymath online mathematical collaborations initiated by Terence Tao and Timothy Gowers
 Martin, Ursula 2016 Computational logic and the social Journal of Logic and Computation, 26, 467477 provides an overview in historical context.
 Martin, Ursula and Pease, Alison 2015 Stumbling around in the dark: lessons from everyday mathematics Springer LNCS, 9195, 29  51 (invited plenary for 25 years of CADE) looks at social machines in the context of formal proof and experimental mathematics
 Martin, Ursula and Pease, Alison 2015, Hardy, Littlewood and Polymath in Mathematics, Substance and Surmise: Views on the Meaning and Ontology of Mathematics, ed Ernest Davis, Philip J. Davis, Springer frames the polymath experiments in the context of G H Hardy's views of collaboration
 Martin, Ursula and Pease, Alison 2012 Seventy four minutes of mathematics: An analysis of the third MiniPolymath project Proceedings of AISB/IACAP 2012, 52105, is a preliminary study of the minipolymath experiments and provides a typology of the mathematical activities they exhibit  proof, examples, concept formation and the like.
 Martin, Ursula and Pease, Alison 2013 What does mathoverflow tell us about the production of mathematics? SOHUMAN workshop at CHI 2013, Paris is a preliminary study of the mathoverflow Q&A site for research mathematics, and provides a typology of questions and answers
 Martin, Ursula and Pease, Alison 2013 Mathematical practice, crowdsourcing, and social machines International Conference on Intelligent Computer Mathematics, Springer 7961, 98119 (invited plenary) lays out the research agenda in the context of formal proof and social machines
Modelling mathematical conversations with argumentation theor y with Alison Pease and Joe Corneli Social machines provide models for mathematical argument using argumentation theory and LSC  the lightweight social calculus.
 Pease, Alison, Corneli, Joseph et al, 2017 Lakatosstyle collaborative mathematics through dialectical, structured and abstract argumentation Artificial Intelligence 246, 181–219
 Corneli, Joseph, Martin, Ursula, Nesin, Gabriela, and Pease, Alison 2017 Modelling polymath coversations in IAT, in preparation
Philosophy for mathematical practice with Andrew Aberdein, Alison Pease and Fenner Tanswell. We use the polymath online mathematical collaborations as an evidence base for understanding mathematical practice, in particular to assess notions of explanation in mathematics, with our most recent paper countering a number of assertions on explanation in the philosophical literature. Fenner Tanswell works on the connection between formal and informal proofs
 Tanswell, Fenner2015 A Problem with the Dependence of Informal Proofs on Formal Proofs Philosophia Mathematica 23, 295310.
 Aberdein, Andrew, Martin, Ursula and Pease, Alison, An empirical invesigation into explanation in mathematical conversations, u nder review
T he nature of mathematical collaboration, an ethnographic appro ach , with Lorenzo Lane. A report was written on collaboration at the Isaac Newton Institute and forms the basis of part of Lane's PhD thesis (University of Edinburgh 2016), with further papers in preparation, details on request.
Mathematics policy and the impact of mathematics, with Laura Meagher. We use materials submitted for the 2014 Research Excellence Framework as an evidence base to assess the mechanisms by which mathematics has impact, highlighting the importance of interdisciplinarity, relationship building and the long term view.
 Meagher, Laura R. and Martin, Ursula, 2017 Slightly dirty maths: The richly textured mechanisms of impact Research Evaluation 26: 1527
 Popular accounts appeared in Times Higher, London Mathematical Society Newsletter, and Mathematics Today magazine, and the work was cited in a number of submissions to the 2017 HEFCE consultation on the REF.
The mathematics of Ada Lovelace, with Christopher Hollings and Adrian Rice In 2015 Ursula Martin organised Oxford's Ada Lovelace bicentenary celebrations, including collaborations with the Bodleian Library, BBC and various science museums. She curated an exhibition, now on display at the Silicon Valley Computer History Museum, and led the digitisation of Ada Lovelace's mathematics, with the support of the Clay Mathematics Institute. Numerous presentations included lectures at the Hay Festival, Computer History Museum and Gresham College.
 Hollings, Christopher; Martin, Ursula, and Rice, Adrian 2017 Ada Lovelace, a mathematical childhood, to appear, Journal of the British Society for the History of Mathematics Covers Lovelace's education before 1840, which encompassed older traditions of practical geometry, newer textbooks influenced by continental approaches, wide reading, and a fascination with machinery, and challenges earlier judgements of her mathematical knowledge and skills which have impacted later scholarly and popular discourse.
 Hollings, Christopher; Martin, Ursula, and Rice, Adrian 2017 The LovelaceDe Morgan Mathematical Correspondence: A Critical ReAppraisal, to appear, Historia Mathematica The first account by historians of mathematics of Lovelace's informal correspondence course with Augustus De Morgan. Detailed contextual analysis gives a corrected ordering of the archive material, and shows Lovelace learning good habits of study, a grounding in certain areas of higher mathematics, a critical attitude towards foundational principles, the ability to make perceptive mathematical observations, and exposure to ideas then current in British mathematical research. Contrary to earlier claims, Lovelace had the mathematical background for her famous 1843 paper, the potential for serious mathematical work.
 Hollings, Christopher; Martin, Ursula, and Rice, Adrian, 2018 A da Lovelace: the education of a computer scientist , illustrated book to be published by the Bodleian Press
 Popular accounts have appeared in London Review of Books, BBC Oxford, EPSRC Blog, EDGE 2017 questions, London Mathematical Society Newsletter, Mathematics Today magazine, CORE magazine (Computer History Museum)
Earlier research
2003 onwards, compuational logic for control A totally novel “block diagram logic” was devised to solve a concrete problem raised by DSTL engineers, and then generalised to the abstract domain of traced monoidal categories. This showed that the new logic, and other results in computer science, are instantiations of this general concept; most strikingly Hoare’s logic of programs, devised in the 1960s, and the foundation of contemporary “industry standard” software verification. The paper received a “Best of 2013” award from the prestigious Computing Reviews journal. The pilot work was funded by QinetiQ, with subsquent funding from EPSRC.
 Arthan, Rob, Martin, Ursula and Oliva, Paulo 2013 A Hoare Logic for linear systems Formal Aspects of Computing, 25, 345363
 Arthan, Rob, Martin, Ursula, Mathiesen, Erik and Oliva, Paulo 2009 A general framework for sound and complete FloydHoare logics, ACM Trans on Computational Logic, 11, 112
 Boulton, Richard, Gottliebsen, Hanne, Hardy, Ruth, Kelsey, Tom and Martin, Ursula 2004 Design verification for control engineering, Integrated Formal Methods, Springer LNCS, 2999, 2135
1997 onwards, combining computational logic and computer algebra This was pioneering in developing new kinds of interface specifications for numerical libraries, which was extended to a new elegant solution to the problem of deficiencies in computer algebra systems, through using restricted calls to and from the Maple computer algebra system to specialist logic algorithms, via a limited interface that shields the user from complexity. The pilot work was developed during a sabbatical at SRI, and subsequently through a collaboration with NASA, with additional funding from EPSRC
 Gottliebsen, Hanne, Hardy, Ruth, Lightfoot Olga and Martin, Ursula 2013 Applications of real number theorem proving in PVS, Formal Aspects of Computing, 25, 9931016
 Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula 2005 Hidden verification for computational mathematics, Journal of Symbolic Computation, 39, 539567
 Dunstan, Martin, Kelsey, Tom, Martin, Ursula and Linton, Steve 1998 Lightweight formal methods for computer algebra, ACM Proceedings on Symbolic and Algebraic Computation, 1998, 8087
1990 onwards, Computer algebra and computational logic Early work included the first application of computational logic in group theory, obtaining results, at the time, well beyond the scope of standard techniques; novel unification algorithms inspired by group theory; and termination algorithms that provided a unified framework for understanding the diverse methods in use at the time.
 Martin, Ursula and Scott, Elizabeth 1997 The order types of termination orderings on monadic terms, strings and multisets, Journal of Symbolic Logic, 62, 624635
 Martin, Ursula and Lai, Mike 1992 Some experiments with a completion theorem prover, Journal of Symbolic Computation, 13, 81100
 Dick, Jeremy, Martin, Ursula and Kalmus, John 1990 Automating the KnuthBendix ordering, Acta Informatica, 28, 95119
 Martin, Ursula and Nipkow, Tobias 1989 Boolean Unification: the story so far, Journal of Symbolic Computation, 7, 275293
 Martin, Ursula 1989 A geometrical approach to multiset orderings, Journal of Theoretical Computer Science, 67, 3754
 Martin, Ursula and Nipkow, Tobias 1988 Unification in Boolean rings, Journal of Automated Reasoning, 4, 381396
1980 onwards, Group theory and combinatorics Research in group theory, combinatorics, and graph theory, mainly concerning symmetries of structures. First published paper, in 1980, provided a novel simple proof of a famous result of Gaschütz: in 2007, with Helleloid at Stanford, showed random groups of certain kinds have very restricted symmetry, a result with powerful implications which is still regularly applied in other domains.
 Helleloid, Geir and Martin, Ursula 2007 The automorphism group of a finite pgroup is almost always a pgroup, Journal of Algebra, 312, 294–329
 Martin, Ursula 1986 Almost all 𝑝groups have automorphism group a 𝑝group Bulletin of the American Mathematical Society, 15, 7882
 Webb, Ursula 1980 An elementary proof of Gaschütz' theorem Archiv der Mathematik 35 (1) 2326
Current research collaborators Andrew Aberdein, Joe Corneli, Chris Hollings, Lorenzo Lane, Laura Meagher, Alison Pease, Adrian Rice, Gabriela RinoNesin, Fenner Tanswell
Former RAs, graduate students and coauthors Andrew Adams, Rob Arthan, Richard Boulton, Muffy Calder, Adam Cichon, Dave Cohen, Victoria Coleman, Nick Cropper, Jeremy Dick, Martin Dunstan, Hanne Gottliebsen, Ruth Hardy, Geir Helleloid, John Kalmus, Tom Kelsey, Mike Lai, Olga Lightfoot, Steve Linton, Athen Ma, Erik Mathiesen, Natasa MilicFrayling, Bill Mitchell, Hanan Mohammed, Kathy Norrie, Tobias Nipkow, Paulo Oliva, Sam Owre, Peter Prohle, Liz Scott, Tim Storer, Duncan Shand, Phil Watson, Jeannette Wing.
Selected Publications

Hardy‚ Littlewood and polymath
Ursula Martin and Alison Pease
In Mathematics‚ Substance and Surmise. Pages 9–23. Springer International Publishing. 2015.
Details about Hardy‚ Littlewood and polymath  BibTeX data for Hardy‚ Littlewood and polymath

Computational logic and the social
Ursula Martin
In Journal of Logic and Computation. Pages exu036. 2014.
Details about Computational logic and the social  BibTeX data for Computational logic and the social

Opportunities and Challenges in 21st Century Mathematical Computation: ICERM Workshop Report
David H Bailey‚ Jonathan M Borwein‚ Olga Caprotti‚ Ursula Martin‚ Bruno Salvy and Michela Taufer
2014.
Details about Opportunities and Challenges in 21st Century Mathematical Computation: ICERM Workshop Report  BibTeX data for Opportunities and Challenges in 21st Century Mathematical Computation: ICERM Workshop Report