Parallelizing an interactive theorem prover : functional programming and proofs with ACL2
Multi-core systems have become commonplace, however, theorem provers often do not take advantage of the additional computing resources in an interactive setting. This research explores automatically using these additional resources to lessen the delay between when users submit conjectures to the th...
Main Author: | Rager, David Lawrence |
---|---|
Format: | Others |
Language: | en_US |
Published: |
2013
|
Subjects: | |
Online Access: | http://hdl.handle.net/2152/19482 |
Similar Items
-
Generating pseudo-random theorems for testing theorem provers
by: Darwish, Nevin Mahmoud, 1952-
Published: (1978) -
Mechanising heterogeneous reasoning in theorem provers
by: Urbas, Matej
Published: (2014) -
A verified framework for symbolic execution in the ACL2 theorem prover
by: Swords, Sol Otis
Published: (2011) -
A self-verifying theorem prover
by: Davis, Jared Curran
Published: (2010) -
Analogical Reasoning in Geometry Proofs
by: Anass Bayag, et al.
Published: (2021-06-01)