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
(34)- Theorem proving modulo
- ELAN from a rewriting logic point of view
- A semantic framework for proof evidence
- Proof certificates for equality reasoning
- Foreword to the special focus on formal proofs for mathematics and computer science
- Certifying Findel derivatives for blockchain
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Regaining cut admissibility in deduction modulo using abstract completion
- Dealing with algebraic expressions over a field in Coq using Maple
- Generation and presentation of formal mathematical documents
- Developments in formal proofs
- A proposal for broad spectrum proof certificates
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Integrating simplex with tableaux
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- scientific article; zbMATH DE number 1342250 (Why is no real title available?)
- scientific article; zbMATH DE number 691421 (Why is no real title available?)
- Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
- scientific article; zbMATH DE number 2102718 (Why is no real title available?)
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Mixing computations and proofs
- LF+ in Coq for "fast and loose" reasoning
- Formal proof
- Formal proof -- theory and practice
- A Dynamic Poincaré Principle
- A certificate-based approach to formally verified approximations
- Proof by computation in the Coq system
- 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
- Extending numeric automation for number theory formalizations in Mizar
- Formal Reasoning Using Distributed Assertions
- Gluing together proof environments: canonical extensions of LF type theories featuring locks
- A definitional implementation of the Lax logical framework \(\mathsf{LLF}_{\mathscr{P}}\) in \texttt{Coq}, for supporting fast and loose reasoning
- Proof synthesis and reflection for linear arithmetic
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)
