Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version)

TL;DR

This paper discusses methods and challenges in verifying the correctness of saturation-based theorem provers, based on experiences with the Vampire prover, highlighting future directions for improved correctness assurance.

Contribution

It presents current techniques for ensuring Vampire's correctness and identifies future challenges to enhance verification processes in saturation-based theorem proving.

Findings

Current correctness techniques for Vampire

Identified challenges in verification processes

Future directions for improved correctness guarantees

Abstract

This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that Vampire is correct and use this to motivate future challenges that need to be addressed to make this process more straightforward and to achieve better correctness guarantees.