pith. sign in

Josef Urban

Identifiers

  • name variant Josef Urban 0.60 · backfill

Papers (37)

  1. Munkres' General Topology Autoformalized in Isabelle/HOL cs.AI · 2026 · author #4
  2. Hammering Mizar by Learning Clause Guidance cs.AI · 2019 · author #2
  3. ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E cs.AI · 2019 · author #4
  4. Reinforcement Learning of Theorem Proving cs.AI · 2018 · author #2
  5. First Experiments with Neural Translation of Informal to Formal Mathematics cs.CL · 2018 · author #3
  6. Machine Learning Guidance and Proof Certification for Connection Tableaux cs.LO · 2018 · author #3
  7. Learning to Reason with HOL4 tactics cs.AI · 2018 · author #3
  8. ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback cs.AI · 2018 · author #2
  9. ENIGMA: Efficient Learning-based Inference Guiding Machine cs.LO · 2017 · author #2
  10. Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving cs.CL · 2016 · author #2
  11. BliStrTune: Hierarchical Invention of Theorem Proving Strategies cs.LO · 2016 · author #2
  12. Monte Carlo Tableau Proof Search cs.LO · 2016 · author #3
  13. DeepMath - Deep Sequence Models for Premise Selection cs.AI · 2016 · author #6
  14. Extending E Prover with Similarity Based Clause Selection Strategies cs.LO · 2016 · author #2
  15. Extracting Higher-Order Goals from the Mizar Mathematical Library cs.LO · 2016 · author #2
  16. A formal proof of the Kepler conjecture math.MG · 2015 · author #20
  17. Certified Connection Tableaux Proofs for HOL Light and TPTP cs.LO · 2014 · author #2
  18. Machine Learning of Coq Proof Guidance: First Experiments cs.LO · 2014 · author #3
  19. Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description cs.AI · 2014 · author #2
  20. Machine Learner for Automated Reasoning 0.4 and 0.5 cs.LG · 2014 · author #2
  21. Learning-assisted Theorem Proving with Millions of Lemmas cs.AI · 2014 · author #2
  22. MizAR 40 for Mizar 40 cs.AI · 2013 · author #2
  23. Lemma Mining over HOL Light cs.AI · 2013 · author #2
  24. HOL(y)Hammer: Online ATP Service for HOL Light cs.AI · 2013 · author #2
  25. MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers cs.AI · 2013 · author #2
  26. Formal Mathematics on Display: A Wiki for Flyspeck cs.MS · 2013 · author #3
  27. BliStr: The Blind Strategymaker cs.AI · 2013 · author #1
  28. Theorem Proving in Large Formal Mathematics as an Emerging AI Field cs.AI · 2012 · author #1
  29. Parallelizing Mizar cs.MS · 2012 · author #1
  30. Point-and-write --- Documenting Formal Mathematics by Reference cs.MS · 2012 · author #3
  31. Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar cs.DL · 2011 · author #3
  32. ATP and Presentation Service for Mizar Formalizations cs.DL · 2011 · author #1
  33. Premise Selection for Mathematics by Corpus Analysis and Kernel Methods cs.LG · 2011 · author #5
  34. Licensing the Mizar Mathematical Library cs.DL · 2011 · author #5
  35. Large Formal Wikis: Issues and Solutions cs.DL · 2011 · author #4
  36. Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar cs.AI · 2010 · author #1
  37. A Wiki for Mizar: Motivation, Considerations, and Initial Prototype cs.DL · 2010 · author #1

Mentions

  • 1301.2683 #1 · backfill · confidence 0.70 Josef Urban
  • 1209.3914 #1 · backfill · confidence 0.70 Josef Urban
  • 1206.0141 #1 · backfill · confidence 0.70 Josef Urban
  • 1204.5094 #3 · backfill · confidence 0.70 Josef Urban
  • 1109.3687 #3 · backfill · confidence 0.70 Josef Urban
  • 1109.0616 #1 · backfill · confidence 0.70 Josef Urban
  • 1108.3446 #5 · backfill · confidence 0.70 Josef Urban
  • 1107.3212 #5 · backfill · confidence 0.70 Josef Urban
  • 1107.3209 #4 · backfill · confidence 0.70 Josef Urban
  • 1005.4592 #1 · backfill · confidence 0.70 Josef Urban
  • 1005.4552 #1 · backfill · confidence 0.70 Josef Urban

Frequent Coauthors