Sökning: WFRF:(Johansson Moa 1981)
> (2013-2014) >
Proof-pattern recog...
Proof-pattern recognition and lemma discovery in ACL2
-
- Heras, J. (författare)
- University of Dundee
-
- Komendantskaya, E. (författare)
- University of Dundee
-
- Johansson, Moa, 1981 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
visa fler...
-
- Maclean, E. (författare)
- University of Edinburgh
-
visa färre...
-
(creator_code:org_t)
- Berlin, Heidelberg : Springer Berlin Heidelberg, 2013
- 2013
- Engelska.
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 8312, s. 389-406
- Relaterad länk:
-
http://dx.doi.org/10...
-
visa fler...
-
http://arxiv.org/pdf...
-
https://doi.org/10.1...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. This paper presents the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
Nyckelord
- Theorem proving
- Lemma discovery
- Pattern recognition
- Analogy
- Statistical machine-learning
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas