Mining the Archive of Formal Proofs
From MaRDI portal
Publication:3453102
DOI10.1007/978-3-319-20615-8_1zbMATH Open1417.68176OpenAlexW1910466616WikidataQ114700358 ScholiaQ114700358MaRDI QIDQ3453102FDOQ3453102
Authors: Jasmin Christian Blanchette, Daniel Matichuk, Tobias Nipkow, Maximilian P. L. Haslbeck 
Publication date: 20 November 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01212594/file/paper.pdf
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
- Title not available (Why is that?)
- MPTP 0.2: Design, implementation, and initial experiments
- System description: E 1.8
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Lightweight relevance filtering for machine-generated resolution problems
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- Extending Sledgehammer with SMT solvers
- Semi-intelligible Isar proofs from machine-generated proofs
- Concrete semantics. With Isabelle/HOL
- Licensing the Mizar Mathematical Library (MML)
- Sledgehammer: judgement day
- A learning-based fact selector for Isabelle/HOL
- A formally verified compiler back-end
- A machine-checked proof of the odd order theorem
- The Isabelle collections framework
- Title not available (Why is that?)
- Java and the Java memory model -- a unified, machine-checked formalisation
Cited In (20)
- A formalization of the Smith normal form in higher-order logic
- An application of proof mining to nonlinear iterations
- Lyndon words formalized in Isabelle/HOL
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Combining higher-order logic with set theory formalizations
- Title not available (Why is that?)
- Developments in formal proofs
- Computer certification of generalized rough sets based on relations
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Re-imagining the Isabelle archive of formal proofs
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Cooperative Repositories for Formal Proofs
- Challenges and experiences in managing large-scale proofs
- Archive Formal Proofs
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Verified reductions for optimization
- Automated Comparative Study of Some Generalized Rough Approximations
- Formalization quality in Isabelle
- Formal entity graphs as complex networks: assessing centrality metrics of the archive of formal proofs
- Engineering mathematics: the odd order theorem proof
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)
