证明器和求解器的验证
Verification of Provers and Solvers
AI总结：
介绍自动推导工具与证明助手的连接方法，通过认证和验证等方式，回顾比较现有方法并提及成功应用。
AI中文摘要：
自动推导工具如自动定理证明器、SAT求解器、SMT求解器和终止分析器可通过多种方法连接到证明助手，特别是通过认证和验证。本章回顾并比较现有方法，并提及一些成功应用。
英文摘要：
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.
