Checking Linear Integer Arithmetic Proofs in Lambdapi

doi:10.1007/978-3-032-04167-8_20

2026-01-01

Alessio Coltellacci

Stephan Merz *

DOI：10.1007/978-3-032-04167-8_20

原文链接

原文求助

摘要

En 中文

现代SMT求解器可以生成不可满足性的证明，以便结果可以独立检查。验证这些证明的一种可靠方法是利用证明助手进行重构。在先前的工作中，SMT检查器Carcara被扩展，以在Lambdapi（一种为互操作性设计的证明助手）中重构SMT证明，支持为与Rocq、Lean或HOL-Light等其他证明助手集成而导入和导出证明。虽然该工作仅限于非算术的SMT理论，但本文提出了一种扩展，能够重构涉及线性整数算术的SMT证明。

Keyword:

SMT

Alethe

integer arithmetic

Lambdapi

normal form

proof by reflection

期刊

FRONTIERS OF COMBINING SYSTEMS, FROCOS 2025

IF:

论文数:

被引数:

机构

universite de lorraine

学者数:

1.8W

论文数: 1.4W

被引数: 27

引用论文

Fast Reflexive Arithmetic Tactics the Linear Case and Beyond 快速自反算术策略：线性情况及更复杂情形

Lecture Notes in Computer Science

IF0

PREAI

Besson,Frédéric

IF0

PREAI

Alethe: Towards a Generic SMT Proof Format (extended abstract)

Electronic Proceedings in Theoretical Computer Science

IF0

2021-07-07

OAAI

Hans-Jörg Schurr; Mathias Fleury; Haniel Barbosa; Pascal Fontaine

IF0

PREAI

IF0

PREAI

A complete and terminating approach to linear integer solving

Journal of Symbolic Computation

IF0

2020-09-01

OAAI

Martin Bromberger; Thomas Sturm; Christoph Weidenbach

Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format

Lecture Notes in Computer Science

IF0

2023-04-22

PREAI

Bruno Andreotti; Hanna Lachnitt; Haniel Barbosa

A framework for defining logics 定义逻辑的框架

Journal of the ACM

IF0

1993-01-02

OAAI

Robert Harper; Furio Honsell; Gordon Plotkin

IF0

PREAI

Proving Termination of Programs Automatically with AProVE 使用AProVE自动证明程序终止性

Lecture Notes in Computer Science

IF0

2014-01-01

PREAI

Jürgen Giesl; Marc Brockschmidt; Fabian Emmes; Florian Frohn; Carsten Fuhs; Carsten Otto; Martin Plücker; Peter Schneider-Kamp; Thomas Ströder; Stephanie Swiderski; René Thiemann

查看更多内容