28 citations · 34 across the 6 of their papers we have counts for
4 papers · 1 filter
Twitch: Learning Abstractions for Equational Theorem Proving
Guy Axelrod, Moa Johansson, Nicholas Smallbone
Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting…
Conjectures, Tests and Proofs: An Overview of Theory Exploration
Moa Johansson, Nicholas Smallbone
A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory ex…
Encoding Monomorphic and Polymorphic Types
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu +1
Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means…
Hipster: Integrating Theory Exploration in a Proof Assistant
Moa Johansson, Dan Rosen, Nicholas Smallbone +1
This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new int…