ACL2

Una de las líneas de trabajo en la automatización del razonamiento es la paralelización de las demostraciones. En dicha línea se inscribe la Tesis doctoral Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2 presentada por David L. Rager en la Univ. de Texas en Austin el pasado 20 de Agosto.

Su resumen es

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 theorem prover and when they receive feedback from the prover that is useful in discovering how to successfully complete the proof of a particular theorem.

This research contributes mechanisms that permit applicative programs to execute in parallel while simultaneously preparing these programs for verification by a semi-automatic reasoning system. It also contributes a parallel version of an automated theorem prover, with management of user interaction issues, such as output and how inherently single-threaded, user-level proof features can be configured for use with parallel computation. Finally, this dissertation investigates the types of proofs that are amenable to parallel execution. This investigation yields the result that almost all proof attempts that require a non-trivial amount of time can benefit from parallel execution. Proof attempts executed in parallel almost always provide the aforementioned feedback sooner than if they executed serially, and their execution time is often significantly reduced.

Las transparencias de la presentación se encuentran aquí.