130 citations · 228 across the 17 of their papers we have counts for
6 papers · 1 filter
Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission
Jesse Alama
When formalizing proofs with interactive theorem provers, it often happens that extra background knowledge (declarative or procedural) about mathematical concepts is employed witho…
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
Jesse Alama, Lionel Mamane, Josef Urban
Two methods for extracting detailed formal dependencies from the Coq and Mizar system are presented and compared. The methods are used for dependency extraction from two large math…
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Jesse Alama, Tom Heskes, Daniel Kühlwein +2
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. A good method for premise selection in complex mathematical…
Licensing the Mizar Mathematical Library
Jesse Alama, Michael Kohlhase, Adam Naumowicz +3
The Mizar Mathematical Library (MML) is a large corpus of formalised mathematical knowledge. It has been constructed over the course of many years by a large number of authors and…
Large Formal Wikis: Issues and Solutions
Jesse Alama, Kasper Brink, Lionel Mamane +1
We present several steps towards large formal mathematical wikis. The Coq proof assistant together with the CoRN repository are added to the pool of systems handled by the general…
mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library
Jesse Alama
The Mizar Mathematical Library (MML) is a rich database of formalized mathematical proofs (see http://mizar.org). Owing to its large size (it contains more than 1100 "articles" sum…