Checking linear integer arithmetic proofs in Lambdapi

DOI10.1007/978-3-032-04167-8_20MaRDI QIDQ6852300zbMATH OpenFDO

Authors Alessio Coltellacci, Stephan Merz

Publication date 26 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-04167-8_20

zbMATH Keywords

Aletheinteger arithmeticLambdapinormal formproof by reflectionSMT

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic in artificial intelligence (68T27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
• A complete and terminating approach to linear integer solving
• A framework for defining logics
• CSI -- a confluence tool
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Encoding type universes without using matching modulo associativity and commutativity
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• On the Implementation of Construction Functions for Non-free Concrete Data Types
• Proving termination of programs automatically with AProVE
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Some Axioms for Mathematics
• The Lean 4 theorem prover and programming language
• The new rewriting engine of dedukti (system description)
• Theorem Proving in Higher Order Logics
• Translating HOL-Light proofs to Coq
• Type safety of rewrite rules in dependent types

Cited in

(1)

• Reconstruction of SMT proofs with Lambdapi

This page was built for publication: Checking linear integer arithmetic proofs in Lambdapi

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