Best-First Rippling. - Moa Johansson 001; Alan Bundy; Lucas Dixon (Reasoning, Action and Interaction in AI Theories and Systems, 2006)

Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery. - Moa Johansson 001; Lucas Dixon; Alan Bundy (Verification, Induction, Termination Analysis, 2010)

Case-Analysis for Rippling and Inductive Proof. - Moa Johansson 001; Lucas Dixon; Alan Bundy (ITP, 2010)

On Interpolation in Decision Procedures. - Maria Paola Bonacina; Moa Johansson 001 (TABLEAUX, 2011)

Conjecture Synthesis for Inductive Theories. - Moa Johansson 001; Lucas Dixon; Alan Bundy (J. Autom. Reason., 2011)

HipSpec: Automating Inductive Proofs of Program Properties. - Koen Claessen; Moa Johansson 001; Dan Rosén; Nicholas Smallbone (ATx/WInG@IJCAR, 2012)

Automating Inductive Proofs Using Theory Exploration. - Koen Claessen; Moa Johansson 001; Dan Rosén; Nicholas Smallbone (CADE, 2013)

Proof-Pattern Recognition and Lemma Discovery in ACL2. - Jónathan Heras; Ekaterina Komendantskaya; Moa Johansson 001; Ewen Maclean (LPAR, 2013)

Proof-Pattern Recognition in ACL2. - Jónathan Heras; Ekaterina Komendantskaya; Moa Johansson 001; Ewen Maclean (CoRR, 2013)

Hipster: Integrating Theory Exploration in a Proof Assistant. - Moa Johansson 001; Dan Rosén; Nicholas Smallbone; Koen Claessen (CICM, 2014)

TIP: Tons of Inductive Problems. - Koen Claessen; Moa Johansson 001; Dan Rosén; Nicholas Smallbone (CICM, 2015)

Conditional Lemma Discovery and Recursion Induction in Hipster. - Irene Lobo Valbuena; Moa Johansson 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

The Theory behind Theory Mine. - Alan Bundy; Flaminia Cavallo; Lucas Dixon; Moa Johansson 001; Roy L. McCasland (IEEE Intell. Syst., 2015)

On Interpolation in Automated Theorem Proving. - Maria Paola Bonacina; Moa Johansson 001 (J. Autom. Reason., 2015)

Interpolation Systems for Ground Proofs in Automated Deduction: a Survey. - Maria Paola Bonacina; Moa Johansson 001 (J. Autom. Reason., 2015)

Proving Type Class Laws for Haskell. - Andreas Arvidsson; Moa Johansson 001; Robin Touche (TFP, 2016)

QuickSpec: a lightweight theory exploration tool for programmers (system demonstration). - Maximilian Algehed; Koen Claessen; Moa Johansson 001; Nicholas Smallbone (Haskell, 2017)

Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System. - Moa Johansson 001 (ITP, 2017)

Quick specifications for the busy programmer. - Nicholas Smallbone; Moa Johansson 001; Koen Claessen; Maximilian Algehed (J. Funct. Program., 2017)

Into the Infinite - Theory Exploration for Coinduction. - Sólrún Halla Einarsdóttir; Moa Johansson 001; Johannes Åman Pohjola (AISC, 2018)

Towards Machine Learning on data from Professional Cyclists. - Agrin Hilmkil; Oscar Ivarsson; Moa Johansson 001; Dan Kuylenstierna; Teun van Erp (CoRR, 2018)

Lemma Discovery for Induction - A Survey. - Moa Johansson 001 (CICM, 2019)

Identifying Cross Country Skiing Techniques Using Power Meters in Ski Poles. - Moa Johansson 001; Marie Korneliusson; Nickey Lizbat Lawrence (NAIS, 2019)

Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing. - Sólrún Halla Einarsdóttir; Nicholas Smallbone; Moa Johansson 001 (IFL, 2020)

Conjectures, Tests and Proofs: An Overview of Theory Exploration. - Moa Johansson 001; Nicholas Smallbone (VPT@ETAPS, 2021)

Towards Learning Abstractions via Reinforcement Learning. - Erik Jergéus; Leo Karlsson Oinonen; Emil Carlsson; Moa Johansson 001 (AIC, 2022)

TriCo - Triple Co-piloting of Implementation, Specification and Tests. - Wolfgang Ahrendt; Dilian Gurov; Moa Johansson 001; Philipp Rümmer (ISoLA (1), 2022)

Sudden Semantic Shifts in Swedish NATO discourse. - Brian Bonafilia; Bastiaan Bruinsma; Denitsa Saynova; Moa Johansson 001 (ACL (student), 2023)

The Effect of Scaling, Retrieval Augmentation and Form on the Factual Consistency of Language Models. - Lovisa Hagström; Denitsa Saynova; Tobias Norlund; Moa Johansson 001; Richard Johansson (EMNLP, 2023)

Exploring Mathematical Conjecturing with Large Language Models. - Moa Johansson 001; Nicholas Smallbone (NeSy, 2023)

Class Explanations: the Role of Domain-Specific Content and Stop Words. - Denitsa Saynova; Bastiaan Bruinsma; Moa Johansson 001; Richard Johansson (NoDaLiDa, 2023)

What Can Large Language Models Do for Theorem Proving and Formal Methods? - Moa Johansson 001 (AISoLA, 2023)

Setting the AI Agenda - Evidence from Sweden in the ChatGPT Era. - Bastiaan Bruinsma; Annika Fredén; Kajsa Hansson; Moa Johansson 001; Pasko Kisic-Merino; Denitsa Saynova (AEQUITAS@ECAI, 2024)

Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods. - George Granberry; Wolfgang Ahrendt; Moa Johansson 001 (IFM, 2024)

Lemma Discovery and Strategies for Automated Induction. - Sólrún Halla Einarsdóttir; Márton Hajdú; Moa Johansson 001; Nicholas Smallbone; Martin Suda 001 (IJCAR (1), 2024)

Towards Integrating Copiloting and Formal Methods - Building Blocks, Architecture, and Challenges. - George Granberry; Wolfgang Ahrendt; Moa Johansson 001 (ISoLA (3), 2024)

Reasoning in Transformers - Mitigating Spurious Correlations and Reasoning Shortcuts. - Daniel Enström; Viktor Kjellberg; Moa Johansson 001 (NeSy (2), 2024)

Can Large Language Models (or Humans) Distill Text? - Nicolas Audinet de Pieuchon; Adel Daoud; Connor Thomas Jerzak; Moa Johansson 001; Richard Johansson (CoRR, 2024)

Learning Efficient Recursive Numeral Systems via Reinforcement Learning. - Jonathan D. Thomas; Andrea Silvi; Devdatt P. Dubhashi; Emil Carlsson; Moa Johansson 001 (CoRR, 2024)

ACE: Abstractions for Communicating Efficiently. - Jonathan D. Thomas; Andrea Silvi; Devdatt P. Dubhashi; Vikas Garg 001; Moa Johansson 001 (CoRR, 2024)

Fact Recall, Heuristics or Pure Guesswork? Precise Interpretations of Language Models for Fact Completion. - Denitsa Saynova; Lovisa Hagström; Moa Johansson 001; Richard Johansson; Marco Kuhlmann (ACL (Findings), 2025)

Identifying Non-Replicable Social Science Studies with Language Models. - Denitsa Saynova; Kajsa Hansson; Bastiaan Bruinsma; Annika Fredén; Moa Johansson 001 (CoRR, 2025)

Lemmanaid: Neuro-Symbolic Lemma Conjecturing. - Yousef Alhessi; Sólrún Halla Einarsdóttir; George Granberry; Emily First; Moa Johansson 001; Sorin Lerner; Nicholas Smallbone (CoRR, 2025)

Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis. - George Granberry; Wolfgang Ahrendt; Moa Johansson 001 (CoRR, 2025)

Benchmarking Debiasing Methods for LLM-based Parameter Estimates. - Nicolas Audinet de Pieuchon; Adel Daoud; Connor T. Jerzak; Moa Johansson 001; Richard Johansson (CoRR, 2025)