28 citations · 34 across the 6 of their papers we have counts for
7 papers
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…
Lemmanaid: Neuro-Symbolic Lemma Conjecturing
Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry +4
Mathematicians and computer scientists are increasingly leveraging proof assistants to formalize and check complex proofs, a task that demands substantial expertise. Can we lower t…
QuickerCheck: Implementing and Evaluating a Parallel Run-Time for QuickCheck
Robert Krook, Nicholas Smallbone, Bo Joel Svensson +1
This paper introduces a new parallel run-time for QuickCheck, a Haskell library and EDSL for specifying and randomly testing properties of programs. The new run-time can run multip…
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…
Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans
Johan Lidén Eddeland, Koen Claessen, Nicholas Smallbone +3
Cyber-Physical Systems (CPSs) are systems with both physical and software components, for example cars and industrial robots. Since these systems exhibit both discrete and continuo…
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…