Autarkic computations in formal proofs
From MaRDI portal
Publication:1610674
DOI10.1023/A:1015761529444zbMath1002.68156OpenAlexW1514486135MaRDI QIDQ1610674
Erik Barendsen, Hendrik Pieter Barendregt
Publication date: 20 August 2002
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1015761529444
Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)
Related Items (20)
LF+ in Coq for "fast and loose" reasoning ⋮ Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Integrating Simplex with Tableaux ⋮ Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants ⋮ Formal and efficient primality proofs by use of computer algebra oracles ⋮ Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs ⋮ A semantic framework for proof evidence ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Theorem proving modulo ⋮ Dealing with algebraic expressions over a field in Coq using Maple ⋮ A certificate-based approach to formally verified approximations ⋮ Proof synthesis and reflection for linear arithmetic ⋮ Proof certificates for equality reasoning ⋮ Regaining cut admissibility in deduction modulo using abstract completion ⋮ Proof by computation in the Coq system ⋮ Plugging-in proof development environments usingLocksinLF ⋮ Certifying Findel derivatives for blockchain ⋮ A Proposal for Broad Spectrum Proof Certificates ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ ELAN from a rewriting logic point of view
Uses Software
This page was built for publication: Autarkic computations in formal proofs
