Verification of Provers and Solvers
Logic in Computer Science
2026-07-28 v1 Symbolic Computation
Abstract
Automatic deduction tools such as automatic theorem provers, SAT (satisfiability) solvers, SMT (satisfiability modulo theories) solvers, and termination analyzers can be connected to proof assistants using various approaches, notably by certification and verification. This chapter reviews and compares the approaches available, and mentions several successful applications.
Cite
@article{arxiv.2607.25793,
title = {Verification of Provers and Solvers},
author = {René Thiemann},
journal= {arXiv preprint arXiv:2607.25793},
year = {2026}
}
Comments
This is Chapter 20 of the Book "Proof Assistants and Their Applications in Mathematics and Computer Science"