Mining the Archive of Formal Proofs

DOI10.1007/978-3-319-20615-8_1zbMath1417.68176OpenAlexW1910466616WikidataQ114700358 ScholiaQ114700358MaRDI QIDQ3453102

Tobias Nipkow, Daniel Matichuk, Jasmin Christian Blanchette, 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

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Related Items

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem, Lyndon words formalized in Isabelle/HOL, Deep Generation of Coq Lemma Names Using Elaborated Terms, The role of the Mizar mathematical library for interactive proof development in Mizar, Computer Certification of Generalized Rough Sets Based on Relations, Formal entity graphs as complex networks: assessing centrality metrics of the archive of formal proofs, Re-imagining the Isabelle archive of formal proofs, Combining higher-order logic with set theory formalizations, Higher-Order Tarski Grothendieck as a Foundation for Formal Proof., Automated Comparative Study of Some Generalized Rough Approximations, Archive Formal Proofs, A formalization of the Smith normal form in higher-order logic

Uses Software

• Isabelle
• Isabelle/HOL
• MPTP 0.2
• VAMPIRE
• SPASS
• Mizar
• z3
• MML
• Sledgehammer
• E Theorem Prover
• HOLyHammer

Cites Work

• Unnamed Item
• Unnamed Item
• Semi-intelligible Isar proofs from machine-generated proofs
• A learning-based fact selector for Isabelle/HOL
• MPTP 0.2: Design, implementation, and initial experiments
• 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
• A formally verified compiler back-end
• System Description: E 1.8
• Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
• Concrete Semantics
• Licensing the Mizar Mathematical Library
• A Machine-Checked Proof of the Odd Order Theorem
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• The Isabelle Collections Framework
• Sledgehammer: Judgement Day