Parallel Verification of Natural Deduction Proof Graphs

James T. Oswald
(Rensselaer Polytechnic Institute)
Brandon Rozek
(Rensselaer Polytechnic Institute)

Graph-based interactive theorem provers offer a visual representation of proofs, explicitly representing the dependencies and inferences between each of the proof steps in a graph or hypergraph format. The number and complexity of these dependency links can determine how long it takes to verify the validity of the entire proof. Towards this end, we present a set of parallel algorithms for the formal verification of graph-based natural-deduction (ND) style proofs. We introduce a definition of layering that captures dependencies between the proof steps (nodes). Nodes in each layer can then be verified in parallel as long as prior layers have been verified. To evaluate the performance of our algorithms on proof graphs, we propose a framework for finding the performance bounds and patterns using directed acyclic network topologies (DANTs). This framework allows us to create concrete instances of DANTs for empirical evaluation of our algorithms. With this, we compare our set of parallel algorithms against a serial implementation with two experiments: one scaling both the problem size and the other scaling the number of threads. Our findings show that parallelization results in improved verification performance for certain DANT instances. We also show that our algorithms scale for certain DANT instances with respect to the number of threads.

In Alberto Ciaffaglione and Carlos Olarte: Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2023), Rome, Italy, 2nd July 2023, Electronic Proceedings in Theoretical Computer Science 396, pp. 36–51.
Published: 17th November 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.396.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org