An interactive SMT tactic in Coq using abductive reasoning

DOI10.29007/432MMaRDI QIDQ7025230zbMATH OpenFDO

Authors Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark Barrett

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/432M

zbMATH Keywords

abductionCoqcvc5SMTCoq

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A generic framework for implicate generation modulo theories
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• A superposition calculus for abductive reasoning
• Automated inference of library specifications for source-sink property verification
• Compositional shape analysis by means of bi-abduction
• Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL
• Extending Sledgehammer with SMT solvers
• Hammer for Coq: automation for dependent type theory
• Hammering towards QED
• scientific article; zbMATH DE number 7178362 (Why is no real title available?)
• Ilinva: using abduction to generate loop invariants
• Maximal specification synthesis
• Overview and evaluation of premise selection techniques for large theory mathematics
• Premise selection for mathematics by corpus analysis and kernel methods
• Prime implicate generation in equational logic
• Satisfiability modulo theories
• Scalable algorithms for abduction via enumerative syntax-guided synthesis

Cited in

(2)

• Theorem proving as constraint solving for coherent logic with function symbols
• Automated completion of statements and proofs in synthetic geometry: an approach based on constraint solving

This page was built for publication: An interactive SMT tactic in Coq using abductive reasoning

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