Due to the difficulty of obtaining formal proofs, there is increasing interest in partially or completely automating proof search in interactive theorem provers. Despite being a theorem prover with an active community and plentiful corpus of 170,000+ theorems, no deep learning system currently exists to help automate theorem proving in ACL2. We have developed a machine learning system that generates recommendations to automatically complete proofs. We show that our system benefits from the copy mechanism introduced in the context of program repair. We make our system directly accessible from within ACL2 and use this interface to evaluate our system in a realistic theorem proving environment.
| Identifer | oai:union.ndltd.org:CALPOLY/oai:digitalcommons.calpoly.edu:theses-4332 |
| Date | 01 June 2023 |
| Creators | Thompson, Robert K, Thompson, Robert K |
| Publisher | DigitalCommons@CalPoly |
| Source Sets | California Polytechnic State University |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Master's Theses |
Page generated in 0.0022 seconds