---
title: "HOL(y)Hammer: Online ATP Service for HOL Light (2013)"
description: "The service also offers Emacs, web and command-line front ends and a local installation option. 37 references, cited by 9 papers here."
authors: ["Cezary Kaliszyk", "Josef Urban"]
year: 2013
venue: "arXiv:1309.4962"
source: "https://arxiv.org/abs/1309.4962"
doi: "10.48550/arxiv.1309.4962"
arxiv: "1309.4962"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2013](https://md.research.elamur.ai/free/en/papers/2013/page/3/) / HOL(y)Hammer: Online ATP Service for HOL Light

# HOL(y)Hammer: Online ATP Service for HOL Light

**Authors:** [Cezary Kaliszyk](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/) and [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/) · **Year:** 2013 · **Venue:** arXiv:1309.4962 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1309.4962) · [PDF](https://arxiv.org/pdf/1309.4962v1) · [DOI 10.48550/arxiv.1309.4962](https://doi.org/10.48550/arxiv.1309.4962) · [arXiv 1309.4962](https://arxiv.org/abs/1309.4962) · [OpenAlex](https://openalex.org/W2949526596)

**Citations:** 4 citations (OpenAlex, 2026-10-14) · [9](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Interactive proof assistants such as HOL Light require users to locate relevant library lemmas and assemble proofs by hand. This becomes costly in very large developments like Flyspeck. The authors turn their earlier offline experiments on large-theory automated reasoning into HOL(y)Hammer, a public online service. Users can submit a conjecture, or upload and update a whole HOL Light project.

For each query, the service extracts symbol-, subterm- and type-based features. Premise selectors trained on all previous proofs then rank useful lemmas, using sparse naive Bayes from SNoW and a distance-weighted k-NN. The top-ranked premises are translated into ATP formats and passed to provers such as Vampire, E and Z3. Successful proofs are minimized and rebuilt as HOL Light tactics. Native decision procedures run alongside in parallel.

Offline evaluation showed that 47% of Flyspeck toplevel theorems can be proved automatically in 30 seconds. The service also offers Emacs, web and command-line front ends and a local installation option. It is a practical step toward a reasoning assistant for formal mathematics, comparable in spirit to Wolfram Alpha.

## Key points
- The server has 48 CPUs and runs 7 AI/ATP combinations plus 4 decision procedures per query. Counting individual prover strategies, this amounts to roughly 70 attempts per query.
- Preloaded libraries include Flyspeck, Multivariate Analysis and Complex Analysis. Users can upload new projects, and content encoding plus checkpointing let earlier proof knowledge be reused across versions.
- The June 2012 Flyspeck version has 14,185 theorems, about 30.000 features per extraction method and 16,082 labels.
  - Push-button success rose from 39% to 47%, using 14 CPUs for 30 seconds each.
  - Training takes about 1 s for k-NN and 6–25 s for naive Bayes.
- The local installation uses naive Bayes on HOL Light proof dependencies and runs Vampire, Eprover and Z3 with three-fold parallelism.
- Planned future work includes:
  - git-based project updates,
  - secure and private uploads,
  - using the system as a semantic layer for parsing informal mathematical texts.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Radboud University Nijmegen](https://md.research.elamur.ai/free/en/universities/radboud-university-nijmegen/) — University, Nijmegen, Netherlands · 26 works · 2,125 citations
- [Universität Innsbruck](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) — University, Innsbruck, Austria · 23 works · 1,475 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Cezary Kaliszyk and Josef Urban. 2013. HOL(y)Hammer: Online ATP Service for HOL Light. arXiv:1309.4962.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{kaliszyk2013hol,
  title = {{HOL(y)Hammer: Online ATP Service for HOL Light}},
  author = {Cezary Kaliszyk and Josef Urban},
  year = {2013},
  doi = {10.48550/arxiv.1309.4962},
  eprint = {1309.4962},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1309.4962}
}
```

- [← previous Chinese Event Coreference Resolution: Understanding the State of the Art](https://md.research.elamur.ai/free/en/papers/chen-2013-chinese-event-coreference-resolution-understanding/)
- [next → A User Study: Technology to Increase Teachers' Linguistic Awareness to Improve Instructional Language Support for English Language Learners](https://md.research.elamur.ai/free/en/papers/burstein-2013-user-study-technology-increase-teachers/)
- [↑ back to papers of 2013](https://md.research.elamur.ai/free/en/papers/2013/page/3/)

## References

37 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Behzad Akbarpour and Lawrence C. Paulson. MetiTarski: An automatic theorem prover for real-valued special functions. J. Autom. Reasoning, 44(3):175–205, 2010. [find](https://scholar.google.com/scholar?q=Behzad+Akbarpour+and+Lawrence+C%2E+Paulson%2E+MetiTarski%3A+An+automatic+theorem+prover+for+real%2Dvalued+special+functions%2E+J%2E+Autom%2E+Reasoning%2C+44%283%29%3A175%E2%80%93205%2C+2010%2E)
2. Jesse Alama, Kasper Brink, Lionel Mamane, and Josef Urban. Large formal wikis: Issues and solutions. In James H. Davenport, William M. Farmer, Josef Urban, and Florian Rabe, editors, Calculemus/MKM, volume 6824 of LNCS, pages 133–148. Springer, 2011. [find](https://scholar.google.com/scholar?q=Jesse+Alama%2C+Kasper+Brink%2C+Lionel+Mamane%2C+and+Josef+Urban%2E+Large+formal+wikis%3A+Issues+and+solutions%2E+In+James+H%2E+Davenport%2C+William+M%2E+Farmer%2C+Josef+Urban%2C+and+Florian+Rabe%2C+editors%2C+Calculemus%2FMKM%2C+v)
3. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. Encoding Monomorphic and Polymorphic Types. In TACAS, 2013. To appear, [http://www21.in.tum.de/˜blanchet/enc_types_paper.pdf](http://www21.in.tum.de/˜blanchet/enc_types_paper.pdf). [↗](http://www21.in.tum.de/˜blanchet/enc_types_paper.pdf)
4. Jasmin Christian Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. Available online at [http://www21.in.tum.de/˜blanchet/tff1spec.pdf](http://www21.in.tum.de/˜blanchet/tff1spec.pdf). [↗](http://www21.in.tum.de/˜blanchet/tff1spec.pdf)
5. Andy Carlson, Chad Cumby, Jeff Rosen, and Dan Roth. The SNoW Learning Architecture. Technical Report UIUCDCS-R-99-2101, UIUC Computer Science Department, 5 1999. [find](https://scholar.google.com/scholar?q=Andy+Carlson%2C+Chad+Cumby%2C+Jeff+Rosen%2C+and+Dan+Roth%2E+The+SNoW+Learning+Architecture%2E+Technical+Report+UIUCDCS%2DR%2D99%2D2101%2C+UIUC+Computer+Science+Department%2C+5+1999%2E)
6. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008. [find](https://scholar.google.com/scholar?q=Leonardo+Mendonc%CC%A7a+de+Moura+and+Nikolaj+Bj%C3%B8rner%2E+Z3%3A+An+Efficient+SMT+Solver%2E+In+C%2E+R%2E+Ramakrishnan+and+Jakob+Rehof%2C+editors%2C+TACAS%2C+volume+4963+of+LNCS%2C+pages+337%E2%80%93340%2E+Springer%2C+2008%2E)
7. Sahibsingh A. Dudani. The distance-weighted k-nearest-neighbor rule. Systems, Man and Cybernetics, IEEE Transactions on, SMC-6(4):325–327, 1976. [find](https://scholar.google.com/scholar?q=Sahibsingh+A%2E+Dudani%2E+The+distance%2Dweighted+k%2Dnearest%2Dneighbor+rule%2E+Systems%2C+Man+and+Cybernetics%2C+IEEE+Transactions+on%2C+SMC%2D6%284%29%3A325%E2%80%93327%2C+1976%2E)
8. Ulrich Furbach and Natarajan Shankar, editors. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of LNCS. Springer, 2006. [find](https://scholar.google.com/scholar?q=Ulrich+Furbach+and+Natarajan+Shankar%2C+editors%2E+Automated+Reasoning%2C+Third+International+Joint+Conference%2C+IJCAR+2006%2C+Seattle%2C+WA%2C+USA%2C+August+17%2D20%2C+2006%2C+Proceedings%2C+volume+4130+of+LNCS%2E+Springer%2C+)
9. Allen Van Gelder and Geoff Sutcliffe. Extending the TPTP language to higher-order logic with automated parser generation. In Furbach and Shankar [8], pages 156–161. [find](https://scholar.google.com/scholar?q=Allen+Van+Gelder+and+Geoff+Sutcliffe%2E+Extending+the+TPTP+language+to+higher%2Dorder+logic+with+automated+parser+generation%2E+In+Furbach+and+Shankar+%5B8%5D%2C+pages+156%E2%80%93161%2E)
10. Thomas C. Hales. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors, Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Ger… [find](https://scholar.google.com/scholar?q=Thomas+C%2E+Hales%2E+Introduction+to+the+Flyspeck+project%2E+In+Thierry+Coquand%2C+Henri+Lombardi%2C+and+Marie%2DFranc%CC%A7oise+Roy%2C+editors%2C+Mathematics%2C+Algorithms%2C+Proofs%2C+volume+05021+of+Dagstuhl+Seminar+Proceedi)
11. John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, FMCAD, volume 1166 of LNCS, pages 265–269. Springer, 1996. [find](https://scholar.google.com/scholar?q=John+Harrison%2E+HOL+Light%3A+A+tutorial+introduction%2E+In+Mandayam+K%2E+Srivas+and+Albert+John+Camilleri%2C+editors%2C+FMCAD%2C+volume+1166+of+LNCS%2C+pages+265%E2%80%93269%2E+Springer%2C+1996%2E)
12. John Harrison. Optimizing Proof Search in Model Elimination. In M. McRobbie and J.K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction, number 1104 in LNAI, pages 313–327. Springer-Verlag, 1996. [find](https://scholar.google.com/scholar?q=John+Harrison%2E+Optimizing+Proof+Search+in+Model+Elimination%2E+In+M%2E+McRobbie+and+J%2EK%2E+Slaney%2C+editors%2C+Proceedings+of+the+13th+International+Conference+on+Automated+Deduction%2C+number+1104+in+LNAI%2C+page)
13. Krystof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, CADE, volume 6803 of LNCS, pages 299–314. Springer, 2011. [find](https://scholar.google.com/scholar?q=Krystof+Hoder+and+Andrei+Voronkov%2E+Sine+qua+non+for+large+theory+reasoning%2E+In+Nikolaj+Bj%C3%B8rner+and+Viorica+Sofronie%2DStokkermans%2C+editors%2C+CADE%2C+volume+6803+of+LNCS%2C+pages+299%E2%80%93314%2E+Springer%2C+2011%2E)
14. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. Accepted to ITP 2013, [http://cl-informatik.uibk.ac.at/˜cek/import.pdf](http://cl-informatik.uibk.ac.at/˜cek/import.pdf). [↗](http://cl-informatik.uibk.ac.at/˜cek/import.pdf)
15. Cezary Kaliszyk and Josef Urban. [Learning-assisted automated reasoning with Flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/). CoRR, abs/1211.7012, 2012.
16. Cezary Kaliszyk and Josef Urban. PRocH: Proof reconstruction for HOL Light. In Maria Paola Bonacina, editor, CADE, volume 7898 of Lecture Notes in Computer Science, pages 267–274. Springer, 2013. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+PRocH%3A+Proof+reconstruction+for+HOL+Light%2E+In+Maria+Paola+Bonacina%2C+editor%2C+CADE%2C+volume+7898+of+Lecture+Notes+in+Computer+Science%2C+pages+267%E2%80%93274%2E+Springer%2C+2013%2E)
17. Cezary Kaliszyk and Josef Urban. Stronger automation for Flyspeck by feature weighting and strategy evolution. In Jasmin Christian Blanchette and Josef Urban, editors, PxTP 2013, volume 14 of EPiC Series, pages 87–95. EasyChair, 2013. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+Stronger+automation+for+Flyspeck+by+feature+weighting+and+strategy+evolution%2E+In+Jasmin+Christian+Blanchette+and+Josef+Urban%2C+editors%2C+PxTP+2013%2C+volume+14+of+EPiC+Ser)
18. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR, volume 7364 of LNCS, pages 378–392. Springer, 2012. [find](https://scholar.google.com/scholar?q=Daniel+Ku%CC%88hlwein%2C+Twan+van+Laarhoven%2C+Evgeni+Tsivtsivadze%2C+Josef+Urban%2C+and+Tom+Heskes%2E+Overview+and+evaluation+of+premise+selection+techniques+for+large+theory+mathematics%2E+In+Bernhard+Gramlich%2C+Dale)
19. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35–60, 2008. [find](https://scholar.google.com/scholar?q=Jia+Meng+and+Lawrence+C%2E+Paulson%2E+Translating+higher%2Dorder+clauses+to+first%2Dorder+clauses%2E+J%2E+Autom%2E+Reasoning%2C+40%281%29%3A35%E2%80%9360%2C+2008%2E)
20. Lawrence C. Paulson and Jasmin Blanchette. Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In 8th IWIL, 2010. Invited talk. [find](https://scholar.google.com/scholar?q=Lawrence+C%2E+Paulson+and+Jasmin+Blanchette%2E+Three+years+of+experience+with+Sledgehammer%2C+a+practical+link+between+automated+and+interactive+theorem+provers%2E+In+8th+IWIL%2C+2010%2E+Invited+talk%2E)
21. Lawrence C. Paulson and Kong Woei Susanto. Source-level proof reconstruction for interactive theorem proving. In Klaus Schneider and Jens Brandt, editors, TPHOLs, volume 4732 of LNCS, pages 232–245. Springer, 2007. [find](https://scholar.google.com/scholar?q=Lawrence+C%2E+Paulson+and+Kong+Woei+Susanto%2E+Source%2Dlevel+proof+reconstruction+for+interactive+theorem+proving%2E+In+Klaus+Schneider+and+Jens+Brandt%2C+editors%2C+TPHOLs%2C+volume+4732+of+LNCS%2C+pages+232%E2%80%93245%2E+S)
22. Andrew Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors, Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993. [find](https://scholar.google.com/scholar?q=Andrew+Pitts%2E+The+HOL+logic%2E+In+M%2E+J%2E+C%2E+Gordon+and+T%2E+F%2E+Melham%2C+editors%2C+Introduction+to+HOL%3A+A+theorem+proving+environment+for+higher+order+logic%2E+Cambridge+University+Press%2C+1993%2E)
23. Alexandre Riazanov and Andrei Voronkov. The design and implementation of VAMPIRE. AI Commun., 15(2-3):91–110, 2002. [find](https://scholar.google.com/scholar?q=Alexandre+Riazanov+and+Andrei+Voronkov%2E+The+design+and+implementation+of+VAMPIRE%2E+AI+Commun%2E%2C+15%282%2D3%29%3A91%E2%80%93110%2C+2002%2E)
24. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. [find](https://scholar.google.com/scholar?q=Stephan+Schulz%2E+E+%2D+A+Brainiac+Theorem+Prover%2E+AI+Commun%2E%2C+15%282%2D3%29%3A111%E2%80%93126%2C+2002%2E)
25. Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Allen Van Gelder. Using the TPTP language for writing derivations and finite interpretations. In Furbach and Shankar [8], pages 67–81. [find](https://scholar.google.com/scholar?q=Geoff+Sutcliffe%2C+Stephan+Schulz%2C+Koen+Claessen%2C+and+Allen+Van+Gelder%2E+Using+the+TPTP+language+for+writing+derivations+and+finite+interpretations%2E+In+Furbach+and+Shankar+%5B8%5D%2C+pages+67%E2%80%9381%2E)
26. Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers. Formal mathematics on display: A wiki for Flyspeck. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, MKM/Calculemus/DML, volume 7961 of Lecture Notes in Computer Science, pages 152–167… [find](https://scholar.google.com/scholar?q=Carst+Tankink%2C+Cezary+Kaliszyk%2C+Josef+Urban%2C+and+Herman+Geuvers%2E+Formal+mathematics+on+display%3A+A+wiki+for+Flyspeck%2E+In+Jacques+Carette%2C+David+Aspinall%2C+Christoph+Lange%2C+Petr+Sojka%2C+and+Wolfgang+Winds)
27. Josef Urban. MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. International Journal on Artificial Intelligence Tools, 15(1):109–130, 2006. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+MoMM+%2D+fast+interreduction+and+retrieval+in+large+libraries+of+formalized+mathematics%2E+International+Journal+on+Artificial+Intelligence+Tools%2C+15%281%29%3A109%E2%80%93130%2C+2006%2E)
28. Josef Urban. An Overview of Methods for Large-Theory Automated Theorem Proving (Invited Paper). In Peter Höfner, Annabelle McIver, and Georg Struth, editors, ATE Workshop, volume 760 of CEUR Workshop Proceedings, pages 3–8. CEUR-WS.org, 2011. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+An+Overview+of+Methods+for+Large%2DTheory+Automated+Theorem+Proving+%28Invited+Paper%29%2E+In+Peter+Ho%CC%88fner%2C+Annabelle+McIver%2C+and+Georg+Struth%2C+editors%2C+ATE+Workshop%2C+volume+760+of+CEUR+Workshop)
29. Josef Urban. Content-based encoding of mathematical and code libraries. In Christoph Lange and Josef Urban, editors, Proceedings of the ITP 2011 Workshop on Mathematical Wikis (MathWikis), number 767 in CEUR Workshop Proceedings, pages 49–53, Aachen, 2011. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+Content%2Dbased+encoding+of+mathematical+and+code+libraries%2E+In+Christoph+Lange+and+Josef+Urban%2C+editors%2C+Proceedings+of+the+ITP+2011+Workshop+on+Mathematical+Wikis+%28MathWikis%29%2C+number+767+)
30. Josef Urban. Parallelizing Mizar. CoRR, abs/1206.0141, 2012. — [arXiv:1206.0141](https://arxiv.org/abs/1206.0141) [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+Parallelizing+Mizar%2E+CoRR%2C+abs%2F1206%2E0141%2C+2012%2E+%E2%80%94+%5BarXiv%3A1206%2E0141%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1206%2E0141%29)
31. Josef Urban. BliStr: The Blind Strategymaker. CoRR, abs/1301.2683, 2013. — [arXiv:1301.2683](https://arxiv.org/abs/1301.2683) [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+BliStr%3A+The+Blind+Strategymaker%2E+CoRR%2C+abs%2F1301%2E2683%2C+2013%2E+%E2%80%94+%5BarXiv%3A1301%2E2683%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1301%2E2683%29)
32. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50:229–241, 2013. [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Piotr+Rudnicki%2C+and+Geoff+Sutcliffe%2E+ATP+and+presentation+service+for+Mizar+formalizations%2E+J%2E+Autom%2E+Reasoning%2C+50%3A229%E2%80%93241%2C+2013%2E)
33. Josef Urban and Geoff Sutcliffe. Automated reasoning and presentation support for formalizing mathematics in Mizar. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, AISC/MKM/Calculemus, volume 6167 of LNCS, pages 132–… [find](https://scholar.google.com/scholar?q=Josef+Urban+and+Geoff+Sutcliffe%2E+Automated+reasoning+and+presentation+support+for+formalizing+mathematics+in+Mizar%2E+In+Serge+Autexier%2C+Jacques+Calmet%2C+David+Delahaye%2C+Patrick+D%2E+F%2E+Ion%2C+Laurence+Ridea)
34. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Geoff+Sutcliffe%2C+Petr+Pudla%CC%81k%2C+and+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2E+MaLARea+SG1+%2D+Machine+Learner+for+Automated+Reasoning+with+Semantic+Guidance%2E+In+Alessandro+Armando%2C+Peter+Baumgartner%2C+and+Gilles+Dow)
35. Josef Urban, Jiřı́ Vyskočil, and Petr Štěpánek. MaLeCoP: Machine learning connection prover. In Kai Brünnler and George Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263–277. Springer, 2011. [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2C+and+Petr+S%CC%8Cte%CC%8Cpa%CC%81nek%2E+MaLeCoP%3A+Machine+learning+connection+prover%2E+In+Kai+Bru%CC%88nnler+and+George+Metcalfe%2C+editors%2C+TABLEAUX%2C+volume+6793+of+LNCS%2C+pages+263%E2%80%93277%2E+Springer%2C)
36. Vernor Vinge. A Fire Upon the Deep. Tor Books, 1992. [find](https://scholar.google.com/scholar?q=Vernor+Vinge%2E+A+Fire+Upon+the+Deep%2E+Tor+Books%2C+1992%2E)
37. Lee Worden. WorkingWiki: a MediaWiki-based platform for collaborative research. In Christoph Lange and Josef Urban, editors, ITP Workshop on Mathematical Wikis (MathWikis), number 767 in CEUR Workshop Proceedings, pages 63–73, Aachen, 2011. Cezary Kaliszyk University of Innsbruck, Austria Josef Urba… [find](https://scholar.google.com/scholar?q=Lee+Worden%2E+WorkingWiki%3A+a+MediaWiki%2Dbased+platform+for+collaborative+research%2E+In+Christoph+Lange+and+Josef+Urban%2C+editors%2C+ITP+Workshop+on+Mathematical+Wikis+%28MathWikis%29%2C+number+767+in+CEUR+Workshop)

*Updated 3 November 2026*