Autarkic computations in formal proofs
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 863013
- Proof theory and automated deduction
- scientific article; zbMATH DE number 978243
- scientific article; zbMATH DE number 2100042
- Automated constructivization of proofs
- scientific article; zbMATH DE number 49488
- scientific article; zbMATH DE number 4043814
- scientific article; zbMATH DE number 3895060
- scientific article; zbMATH DE number 4117898
- Automating theories in intuitionistic logic
Cited in
(31)- Integrating simplex with tableaux
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
- A Dynamic Poincaré Principle
- Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
- Generation and presentation of formal mathematical documents
- Dealing with algebraic expressions over a field in Coq using Maple
- A proposal for broad spectrum proof certificates
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- Foreword to the special focus on formal proofs for mathematics and computer science
- Developments in formal proofs
- scientific article; zbMATH DE number 2102718 (Why is no real title available?)
- Formal and efficient primality proofs by use of computer algebra oracles
- A certificate-based approach to formally verified approximations
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Proof synthesis and reflection for linear arithmetic
- Certifying Findel derivatives for blockchain
- LF+ in Coq for "fast and loose" reasoning
- Formal proof
- Formal proof -- theory and practice
- scientific article; zbMATH DE number 691421 (Why is no real title available?)
- ELAN from a rewriting logic point of view
- Proof by computation in the Coq system
- Formal Reasoning Using Distributed Assertions
- Theorem proving modulo
- Regaining cut admissibility in deduction modulo using abstract completion
- A semantic framework for proof evidence
- Proof certificates for equality reasoning
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Mixing computations and proofs
- Extending numeric automation for number theory formalizations in Mizar
This page was built for publication: Autarkic computations in formal proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1610674)
