I am currently an Associate Professor (Docent) at the Departement of Computer Science and Engineering at Chalmers University in Gothenburg, Sweden. My research interests include an diverse mix of applications of AI: from maths and automated reasoning to sports science and natural language processing for political science.
I am also the Director of the Chalmers MSc programme in Algorithms, Languages and Logic.
In the past, I've been a postdoc at the University of Verona in Italy (2009-2011). I did my PhD in the Mathematical Reasoning Group at the University of Edinburgh (graduated 2009).
Bias and methods of AI technology studying political behavior (2020 - 2024)
Together with Annika Freden (KAU). This project is funded by WASP-HS and will investigate how political scientist can use state-of-the-art AI technology as a tool in their research. A project description can be found on the WASP-HS site. PhD student Denitsa Saynova is funded by this project.
Learning and Exploration in Automated Theorem
Proving (June 2015 - Dec 2021)
Project grant for young researchers by Vetenskapsrådet (the Swedish Research Council). This project investigates how techniques we automatically can discover conjectures about programs or mathematical structures using a technique called theory exploration.
Automated Reasoning About Recursive Programs
(Oct 2011 - June 2015)
This project was funded by a VINNMER Marie Curie Fellowship. It aimed at developing automated reasoning tools for proving properties about recursive programs. Such properties needs to be proved by induction, which in turn often requires discovery of auxillary lemmas. We used theory exploration techniques for this purpose, thus enhancing the power of an automated inductive prover by automatically creating a richer background theory. We implemented these ideas in the HipSpec system, which is an automated inductive prover for Haskell.
Reasoning for Program Analysis (Oct 2009 -
I was a postdoc researcher at the University of Verona working with Maria Paola Bonacina. We developed a technique for computing interpolants from proofs in the superposition calculus and for DPLL(Gamma + T), which combines a first order superpositon prover with a SMT-sovler.
Discovery of Inductive Lemmas (Sept 2005 - June 2009)
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.
TRACKS project course: Digitalisation in Sports (Autumn 2020-)
I teach and supervise student projects primarily related to machine learning on sports data.
and Philosophy of Computing (Spring 2015)
I lead a PhD-level seminar course about ethics and IT that started in April 2015. Due to lack of funding, this course is not currently running.
Testing, Debugging and Verification (2012-2014, 2019)
This is an undergraduate course introducing students to concepts in both testing and debugging, as well as formal specification and program verification techniques.
Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing Solrun Halla Einarsdottir, Nicholas Smallbone and Moa Johansson. Proceedings of IFL'20, 2021. [pdf]
Identifying cross country skiing techniques using power meters in ski poles.
Moa Johansson, Marie Korneliusson and Nickey Lizbat Lawrence.
Proceedings of the Norwegian AI Society Symposium, 2019.
A longer version is also available at ArXiv.
Lemma Discovery for Induction - A Survey Moa Johansson. Proceedings of the Conference on Intelligent Computer Mathematics (CICM). LNAI 11617, Springer, 2019. [pdf]
Into the Infinite - Theory Exploration for Coinduction. Solrun Halla Einarsdottir, Moa Johansson and Johannes Aman Pohjala. Conference on Artificial Intelligence and Symbolic Computation (AISC), 2018. [pdf]
Towards Machine Learning on Data from Professional Cyclists. Agrin Hilmkil, Oscar Ivarsson, Moa Johansson, Dan Kuylenstierna, Teun van Erp. World Congress on Performance Analysis in Sports, 2018. [pdf]
QuickSpec: a lightweight theory exploration tool for programmers (system demonstration) Maximilian Algehed, Koen Claessen, Moa Johansson, Nicholas Smallbone ACM SIGPLAN Notices 52 (10), p. 38-39, 2017.
Automated Theory Exploration for Interactive Theorem Proving. Moa Johansson. Conference on Interactive Theorem Proving (ITP), p. 1-11, 2017. (Invited Talk) [pdf]
Quick Specifications for the Busy Programmer. Nicholas Smallbone, Moa Johansson, Koen Claesson and Maximilian Algehed. Journal of Functional Programming, 2017. Pre-print: [pdf]
Proving Type Class Laws for Haskell. Andreas Arvidsson, Moa Johansson and Robin Touche. Post-proceedings of the Symposium for Trends in Functional Programming 2016. [pdf]
Conditional Lemma Discovery and Recursion Induction in Hipster. Irene Lobo Valbuena and Moa Johansson. Proceedings of the International Workshop on Automated Verification of Critical Systems (AVoCS). Electronic Communications of the EASST, volume 72, 2015. [pdf]
TIP: Tons of Inductive Problems. Moa Johansson, Dan Rosén, Nicholas Smallbone and Koen Claessen. Proceedings of the Conference on Intelligent Computer Mathematics (CICM) 2015. LNAI 9150, p. 333-337, 2015. [pdf].
The Theory Behind TheoryMine. Alan Bundy, Flaminia Cavallo, Lucas Dixon, Moa Johansson and Roy McCasland. IEEE Intelligent Systems, 30(4), p. 64-69, 2015. [pre-print pdf].
Interpolation Systems for Ground Proofs in Automated Deduction: A Survey. Maria Paola Bonacina and Moa Johansson. Journal of Automated Reasoning 54(4), p. 353-390, Springer, 2015. [pdf]
On Interpolation in Automated Theorem Proving. Maria Paola Bonacina and Moa Johansson. Journal of Automated Reasoning 54(1), p. 69-97, Springer, 2015. [pdf]
Hipster: Integrating Theory Exploration in a Proof Assistant. Moa Johansson, Dan Rosén, Nicholas Smallbone and Koen Claessen. Proceedings of the Conference on Intelligent Computer Mathematics (CICM) 2014. LNCS 8543, p. 108-122. Springer. Best paper award. [pdf]
Proof Pattern Recognition and Lemma Discovery in ACL2. Jonathan Heras, Ekaterina Komendantskaya, Moa Johansson and Ewen Maclean. Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) 2013. LNCS 8312, p. 389-406. Springer. [pdf]
Automating Inductive Proofs using Theory Exploration. Koen Claessen, Moa Johansson, Dan Rosén and Nicholas Smallbone. Proceedings of the Conference on Automated Deduction (CADE) 2013. LNCS 7898, p. 392-406. Springer. [pdf].
On Interpolation in Decision Procedures. Maria Paola Bonacina and Moa Johansson. Proceedings of TABLEUX, 2011. LNAI 6793, p. 1-6. Springer [pdf]
Towards Interpolation in an SMT-solver with Integrated Superposition. Maria Paola Bonacina and Moa Johansson. SMT Workshop, 2011, Snowbird Utah. [pdf]
Conjecture Synthesis for Inductive Theories. Moa Johansson, Lucas Dixon and Alan Bundy. Journal of Automated Reasoning 47(3) p. 251-289, 2011. [pdf].
Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery. Moa Johansson, Lucas Dixon and Alan Bundy. Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday, 2010. LNCS 6463, p. 102-116. Springer [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, p. 291-306. Springer [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, p. 83-100, Springer Verlag, 2006. Also presented at the STRATEGIES workshop at FLoC 2006 in Seattle. [pdf]
Selected Workshops, Technical Reports and Draft Papers
Automated Conjecturing in QuickSpec. Moa Johansson and Nicholas Smallbone. 1st Mathematical Reasoning in General Artificial Intelligence Workshop, ICLR 2021. [pdf]
Learning and Exploration in Automated Theorem Proving. Moa Johansson. 6th International Workshop on Aritifical Intelligence for Formal Methods (AI4FM), Edinburgh, UK. 2015. [pdf, 3 pages]
Theory Exploration for Interactive Theorem Proving. Moa Johansson. 4th International Workshop on Aritifical Intelligence for Formal Methods (AI4FM), at ITP Rennes, France. 2013. [pdf, 3 pages]
HipSpec: Automating Inductive Proofs of Program Properties. Koen Claessen, Moa Johansson, Dan Rosén and Nicholas Smallbone. Workshop on Automated Theory Exploration (ATX), at IJCAR Manchester, UK, 2012. [pdf]
A Calculus for Conjecture Synthesis. Moa Johansson, Lucas Dixon and Alan Bundy. Workshop on Automated Mathematical Theory Exploration (AUTOMATHEO), 2010. [pdf].
IsaCoSy: Synthesis of Inductive Theorems. Moa Johansson, Lucas Dixon and Alan Bundy. 1st International Workshop on Automated Mathematical Theory Exploration (AUTOMATHEO), Hagenberg, Austria, 2009. [pdf, 4 pages]
Proof Critics in IsaPlanner. Moa Johansson. Isabelle Workshop 2007, Bremen, Germany. [pdf, pages 56 - 59]
IsaPlanner 2: A Proof Planner in Isabelle. Lucas Dixon and Moa Johansson. School of Informatics Technical Report 1302, University of Edinburgh, 2007 [pdf, 5 pages]
Automated Discovery of Inductive Lemmas. Moa Johansson. School of Informatics, University of Edinburgh, 2009 [pdf]