Output details
11 - Computer Science and Informatics
University of Edinburgh
Output title
A Combinator Language for Theorem Discovery
Type
E - Conference contribution
Name of conference/published proceedings
Intelligent Computer Mathematics
Volume number
7362
Issue number
-
First page of article
371
ISSN of proceedings
0302-9743
Year of publication
2012
Number of additional authors
1
Additional information
<11> Originality: This is a new, generic approach to proof discovery for interactive theorem proving. A combinator language is defined that allows users to write discoverers that collaborate intelligently and concurrently during interactive proofs by doing automatic, background discovery of lemmas based on the current proof context.
Significance: The methodology, which improves the level of automation during interactive proofs, is domain-agnostic and system-independent, and is thus applicable to a range of proof assistants.
Rigour: This is a fully-expansive (LCF-style) framework and it is released as part of the official distribution of the HOL Light theorem prover.
Interdisciplinary
-
Cross-referral requested
-
Research group
A - Centre for Intelligent Systems & their Applications
Citation count
0
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
