Scholarlink

<p>The Alethe format has been adopted by several SMT solvers for explaining why a set of constraints is unsatisfiable. We describe how to interpret Alethe proof traces and generate corresponding proofs that are accepted by the Lambdapi proof checker, a foundational proof assistant based on dependent type theory and rewriting that is intended to serve as a pivot for exchanging proofs between interactive proof assistants. We give an overview of the encoding of SMT logic and of Alethe proof traces in Lambdapi and present results of the evaluation of the checker on benchmark examples.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Reconstruction of SMT proofs with Lambdapi

  • 期刊论文

  • 发表日期：

    2026年2月23日

查看全文
  • Alessio Coltellacci,
  • Bruno Andreotti,
  • Haniel Barbosa,
  • Gilles Dowek,
  • Stephan Merz

摘要

The Alethe format has been adopted by several SMT solvers for explaining why a set of constraints is unsatisfiable. We describe how to interpret Alethe proof traces and generate corresponding proofs that are accepted by the Lambdapi proof checker, a foundational proof assistant based on dependent type theory and rewriting that is intended to serve as a pivot for exchanging proofs between interactive proof assistants. We give an overview of the encoding of SMT logic and of Alethe proof traces in Lambdapi and present results of the evaluation of the checker on benchmark examples.