Reconstruction of SMT proofs with Lambdapi

DOI10.1007/S00236-025-00515-WMaRDI QIDQ6844157zbMATH OpenFDO

Authors Alessio Coltellacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz

Publication date 16 March 2026

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/S00236-025-00515-W

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
• A framework for defining logics
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Checking linear integer arithmetic proofs in Lambdapi
• CSI -- a confluence tool
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Encoding type universes without using matching modulo associativity and commutativity
• Extending Sledgehammer with SMT solvers
• Fast LCF-Style Proof Reconstruction for Z3
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Flexible proof production in an industrial-strength SMT solver
• Hammer for Coq: automation for dependent type theory
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• Logics of specification languages
• On the Implementation of Construction Functions for Non-free Concrete Data Types
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Scalable fine-grained proofs for formula processing
• Theorem Proving in Higher Order Logics
• TLA +  Proofs
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo

This page was built for publication: Reconstruction of SMT proofs with Lambdapi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6844157)