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.

翻译：基于图的交互式定理证明器以可视化方式表示证明，通过图或超图格式显式展示各证明步骤之间的依赖关系和推理过程。这些依赖链接的数量与复杂度决定了验证整个证明有效性的时间。为此，我们提出一组用于形式化验证基于图的自然演绎（ND）风格证明的并行算法。我们引入了分层定义，该定义捕捉了证明步骤（节点）之间的依赖关系。只要先前的层次已被验证，每个层次中的节点即可并行验证。为评估算法在证明图上的性能，我们提出一个框架，利用有向无环网络拓扑（DANTs）寻找性能边界与模式。该框架使我们能够创建具体的DANT实例，用于算法的实证评估。通过此框架，我们将并行算法集与串行实现进行两项实验对比：一项扩展问题规模，另一项扩展线程数量。结果表明，针对特定DANT实例，并行化能提升验证性能。我们还发现，对于某些DANT实例，我们的算法在线程数量的扩展性上表现良好。