We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Conjectures, Tests and Proofs: An Overview of Theory Exploration

Authors: Moa Johansson (Chalmers University of Technology), Nicholas Smallbone (Chalmers University of Technology)
Abstract: 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 exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the user's choice.
Comments: In Proceedings VPT 2021, arXiv:2109.02001
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Programming Languages (cs.PL); Logic (math.LO)
Journal reference: EPTCS 341, 2021, pp. 1-16
DOI: 10.4204/EPTCS.341.1
Cite as: arXiv:2109.03721 [cs.LO]
  (or arXiv:2109.03721v1 [cs.LO] for this version)

Submission history

From: EPTCS [view email]
[v1] Tue, 7 Sep 2021 01:57:07 GMT (53kb,D)

Link back to: arXiv, form interface, contact.