Mining the Archive of Formal Proofs
From MaRDI portal
Publication:3453102
Recommendations
- Re-imagining the Isabelle archive of formal proofs
- scientific article; zbMATH DE number 2174396
- Formal proof -- theory and practice
- An application of proof mining to nonlinear iterations
- New Computational Paradigms
- Towards a formally verified proof assistant
- Explicit Proofs in Formal Provability Logic
- scientific article; zbMATH DE number 3922641
Cites work
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 2110621 (Why is no real title available?)
- A formally verified compiler back-end
- A learning-based fact selector for Isabelle/HOL
- A machine-checked proof of the odd order theorem
- ATP and presentation service for Mizar formalizations
- Concrete semantics. With Isabelle/HOL
- Extending Sledgehammer with SMT solvers
- HOL(y)Hammer: online ATP service for HOL Light
- Java and the Java memory model -- a unified, machine-checked formalisation
- Licensing the Mizar Mathematical Library (MML)
- Lightweight relevance filtering for machine-generated resolution problems
- MPTP 0.2: Design, implementation, and initial experiments
- Semi-intelligible Isar proofs from machine-generated proofs
- Sledgehammer: judgement day
- System description: E 1.8
- The Isabelle collections framework
- Type classes and filters for mathematical analysis in Isabelle/HOL
Cited in
(20)- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Verified reductions for optimization
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Lyndon words formalized in Isabelle/HOL
- Formal entity graphs as complex networks: assessing centrality metrics of the archive of formal proofs
- Challenges and experiences in managing large-scale proofs
- Automated Comparative Study of Some Generalized Rough Approximations
- Combining higher-order logic with set theory formalizations
- scientific article; zbMATH DE number 1951637 (Why is no real title available?)
- Archive Formal Proofs
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Re-imagining the Isabelle archive of formal proofs
- Engineering mathematics: the odd order theorem proof
- A formalization of the Smith normal form in higher-order logic
- Cooperative Repositories for Formal Proofs
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Formalization quality in Isabelle
- An application of proof mining to nonlinear iterations
- Developments in formal proofs
- Computer certification of generalized rough sets based on relations
Describes a project that uses
Uses Software
This page was built for publication: Mining the Archive of Formal Proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453102)
