Abstrakt. Vi presenterar en ny teknik för att kombinera statistisk maskininlärning för korrektur-mönster erkännande med symboliska metoder för lemma upptäckt. Det resulterande verktyget, ACL2(ml), samlar in korrekt statistik och använder statistisk mönsterigenkänning för att förbehandla data från bibliotek, och sedan föreslår extra lemmas i nya bevis genom analogi med redan sett exempel. I detta dokument presenteras genomförandet av ACL2(ml) tillsammans med teoretiska beskrivningar av de bevis-mönsterigenkännings- och lemmaupptäcktsmetoder som ingår i det.
Statistisk maskininlärning användes för att stödja extra lemma formulering analogt i inställningen av ACL2, se REF.
Proof-Pattern Recognition and Lemma Discovery in ACL2
{'venue': 'LPAR', 'journal': None, 'mag_field_of_study': ['Mathematics', 'Computer Science']}