You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Dundee » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Dundee

Return to search Previous output Next output

Output 0 of 0 in the submission

Output title

Proof-Pattern Recognition and Lemma Discovery in ACL2

Type

E - Conference contribution

DOI

Name of conference/published proceedings

Logic for Programming, Artificial Intelligence, and Reasoning Logic for Programming, Artificial Intelligence, and Reasoning : 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013, Proceedings

Volume number

8312

Issue number

First page of article

389

ISSN of proceedings

Year of publication

2013

URL

http://www.springer.com/computer/swe/book/978-3-642-45220-8

Number of additional authors

Additional information

<11> The paper proposes a pioneering method to combine statistical and symbolic machine-learning techniques to process big libraries of computer proofs and discover new lemmas. The publication also presents full implementation of this method as ACL2(ml) programming environment. The work is a result of collaboration between Dundee, Edinburgh and Chalmers, funded by Komendantskaya’s First Grant (EP/J014222/1,£120K), as well as EPSRC EP/H024204/1, £514K and ERC Marie Curie, £200K. The significance of the results has been acknowledged by SICSA Industrial Proof of Concept grant (PI Komendantskaya) with partners the leading Formal-methods industries Centaur Technologies and Rockwell Collins.

Interdisciplinary

Cross-referral requested

Research group

None

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract