Moa Johansson

I am currently a postdoc researcher at the Departement of Informatics at Universita degli Studi di Verona in Italy. I did my PhD in the Mathematical Reasoning Group at the University of Edinburgh.

Research Projects

Reasoning for Program Analysis
This is the postdoc project just starting in Verona, led by Maria Paola Bonacina. More info to come!

Automated Discovery of Inductive Lemmas
For my PhD, I developed new techniques for improving automation of inductive proofs in the IsaPlanner system. I have implemented proof-critics that use information from failed proof attempts to suggest patches, such as introducing a case-split or finding missing lemmas. I have also implemented a system, called IsaCoSy, for synthesising theorems about recursive datatypes and functions. It can help form a useful background theory, reducing the need to search for missing lemmas during later proofs.

Best-First Rippling
I implemented a best-first version of the rippling heuristic in IsaPlanner for my final year undergraduate project.

Publications

Conjecture Synthesis for Inductive Theories. Moa Johansson, Lucas Dixon and Alan Bundy. Submitted to the Journal of Automated Reasoning. To appear [pdf]. Technical Report with complementary proofs: [pdf]

Case-Analysis for Rippling and Inductive Proof. Moa Johansson, Lucas Dixon and Alan Bundy. Proceedings of the Interactive Theorem Proving Conference (ITP), 2010. LNCS 6172. Springer [pdf]

IsaPlanner 2: A Proof Planner in Isabelle. Lucas Dixon and Moa Johansson. School of Informatics Technical Report 1302, University of Edinburgh, 2007 [pdf]

Best-First Rippling. Moa Johansson, Alan Bundy and Lucas Dixon. Reasoning Action and Interaction in AI Theories and Systems - Essays Dedicated to Luigia Carlucci Aiello, pp 83--100, Springer Verlag, 2006. A revised version was also presented at the STRATEGIES workshop at FLoC 2006 in Seattle. [pdf]

Thesis

PhD thesis: Automated Discovery of Inductive Lemmas. Moa Johansson. School of Informatics, University of Edinburgh, 2009 [pdf]

Workshops

IsaCoSy: Synthesis of Inductive Theorems. Moa Johansson, Lucas Dixon and Alan Bundy. 1st International Workshop on Automated Mathematical Theory Exploration, Hagenberg, Austria, 2009. [pdf, 4 pages]

Discovery of Higher-Order Lemmas for Induction. Moa Johansson. CIAO 2008, Darmstadt, Germany.

Proof Critics in IsaPlanner. Moa Johansson. Isabelle Workshop 2007, Bremen, Germany. [pdf, pages 56 - 59]

Proof Critics for IsaPlanner. Moa Johansson, Lucas Dixon and Alan Bundy. Automated Reasoning Workshop 2007, Imperial College, London, UK. [pdf]

Lemma Speculation in Higher-Order Logic. Moa Johansson. CIAO 2007, Brechin, UK.

Proof Critics in IsaPlanner. Moa Johansson. CIAO 2006, Braunhausen, Germany.

A Best-First Planner for Rippling. Moa Johansson. Automated Reasoning Workshop 2005, University of Edinburgh, UK.

Dipartimento Informatica
Universita degli Studi di Verona
Strada le Grazie 15 (room 1.80)
371 34 Verona
Italy

E-mail: moakristin.johansson
  @univr.it