Reasoning for Program Analysis
This is the postdoc project just starting in Verona, led by Maria Paola Bonacina. More info to come!
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.
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]
PhD thesis: Automated Discovery of Inductive Lemmas. Moa Johansson. School of Informatics, University of Edinburgh, 2009 [pdf]
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.