Moa Johansson
Title
Cited by
Cited by
Year
Automating inductive proofs using theory exploration
K Claessen, M Johansson, D Rosén, N Smallbone
Automated Deduction–CADE-24, 392-406, 2013
842013
Conjecture synthesis for inductive theories
M Johansson, L Dixon, A Bundy
Journal of Automated Reasoning 47 (3), 251-289, 2011
842011
Proof-pattern recognition and lemma discovery in ACL2
J Heras, E Komendantskaya, M Johansson, E Maclean
International Conference on Logic for Programming Artificial Intelligence …, 2013
442013
Hipster: Integrating Theory Exploration in a Proof Assistant
M Johansson, D Rosén, N Smallbone, K Claessen
Conference on Intelligent Computer Mathematics (CICM), 2014
402014
TIP: Tons of Inductive Problems
K Claessen, M Johansson, D Rosén, N Smallbone
Conference on Intelligent Computer Mathematics, 2015
312015
Case-Analysis for Rippling and Inductive Proof
M Johansson, L Dixon, A Bundy
Interactive Theorem Proving, 291-306, 2010
272010
HipSpec: Automating Inductive Proofs of Program Properties.
K Claessen, M Johansson, D Rosén, N Smallbone
ATx/WInG@ IJCAR, 16-25, 2012
222012
On interpolation in automated theorem proving
MP Bonacina, M Johansson
Journal of automated reasoning 54 (1), 69-97, 2015
212015
On interpolation in decision procedures
M Bonacina, M Johansson
Automated Reasoning with Analytic Tableaux and Related Methods, 1-16, 2011
162011
Quick specifications for the busy programmer
N Smallbone, M Johansson, K Claessen, M Algehed
Journal of Functional Programming 27, 2017
152017
Interpolation systems for ground proofs in automated deduction: a survey
MP Bonacina, M Johansson
Journal of Automated Reasoning 54 (4), 353-390, 2015
152015
Dynamic rippling, middle-out reasoning and lemma discovery
M Johansson, L Dixon, A Bundy
Verification, Induction, Termination Analysis - Festschrift for Christoph …, 2010
11*2010
Automated discovery of inductive lemmas
M Johansson
PhD. thesis, University of Edinburgh, 2009
112009
Automated theory exploration for interactive theorem proving
M Johansson
International Conference on Interactive Theorem Proving, 1-11, 2017
82017
IsaPlanner 2: A proof planner in Isabelle
L Dixon, M Johansson
DReaM Technical Report (System description), 2007
82007
Conditional Lemma Discovery and Recursion Induction in Hipster
I Lobo Valbuena, M Johansson
15th International Workshop on Automated Verification of Critical Systems …, 2015
7*2015
Towards interpolation in an SMT solver with integrated superposition
MP Bonacina, M Johansson
Notes of the 9th International Workshop on Satisfiability Modulo Theories …, 2011
52011
Best-first rippling
M Johansson, A Bundy, L Dixon
Reasoning, Action and Interaction in AI theories and Systems, 83-100, 2006
42006
Lemma discovery for induction
M Johansson
International Conference on Intelligent Computer Mathematics, 125-139, 2019
32019
Proving Type Class Laws for Haskell
A Arvidsson, M Johansson, R Touche
International Symposium on Trends in Functional Programming, 61-74, 2016
32016
The system can't perform the operation now. Try again later.
Articles 1–20