Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Institution
- Keyword
Articles 1 - 2 of 2
Full-Text Articles in Logic and Foundations
Deep Learning Recommendations For The Acl2 Interactive Theorem Prover, Robert K. Thompson, Robert K. Thompson
Deep Learning Recommendations For The Acl2 Interactive Theorem Prover, Robert K. Thompson, Robert K. Thompson
Master's Theses
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 …
Computable Linear Orders And Turing Reductions, Whitney P. Turner
Computable Linear Orders And Turing Reductions, Whitney P. Turner
Master's Theses
This thesis explores computable linear orders through Turing Reductions and codes zero jump and zero double jump into linear orders using discrete, dense, and block linear relations.