149 citations · 825 across the 48 of their papers we have counts for
5 papers · 1 filter
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…
ATP and Presentation Service for Mizar Formalizations
Josef Urban, Piotr Rudnicki, Geoff Sutcliffe
This paper describes the Automated Reasoning for Mizar (MizAR) service, which integrates several automated reasoning, artificial intelligence, and presentation tools with Mizar and…
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…