Travelled to:1 × Australia
1 × France
1 × Germany
1 × USA
1 × United Kingdom
Collaborated with:C.Kaliszyk D.Kühlwein G.Sutcliffe S.Schulz J.Vyskocil B.Piotrowski E.Tsivtsivadze T.Heskes M.F.0002 P.Pudlák S.S.0001 A.Pease K.Chvalovský J.Jakubuv M.S.0001 T.v.Laarhoven H.Geuvers C.E.Brown T.Gauthier
Talks about:guidanc (2) select (2) reason (2) premis (2) proof (2) autom (2) larg (2) atp (2) reconstruct (1) inconsist (1)
Person: Josef Urban
DBLP: Urban:Josef
Contributed to:
20152013
2012
20112008201720182019Wrote 11 papers:
- CADE-2015-KaliszykSUV
- System Description: E.T. 0.1 (CK, SS, JU, JV), pp. 389–398.
- CADE-2013-KaliszykU #named #proving #re-engineering
- PRocH: Proof Reconstruction for HOL Light (CK, JU), pp. 267–274.
- CADE-2013-KuhlweinSU
- E-MaLeS 1.1 (DK, SS, JU), pp. 407–413.
- IJCAR-2012-KuhlweinLTUH #evaluation #overview #scalability
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics (DK, TvL, ET, JU, TH), pp. 378–392.
- KDIR-2011-KuhlweinUTGH #automation #multi #ranking #reasoning
- Multi-output Ranking for Automated Reasoning (DK, JU, ET, HG, TH), pp. 42–51.
- IJCAR-2008-UrbanSPV #automation #reasoning #semantics
- MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance (JU, GS, PP, JV), pp. 441–456.
- CADE-2017-0001SUP #consistency #detection #first-order #knowledge base #nondeterminism #scalability
- Detecting Inconsistencies in Large First-Order Knowledge Bases (SS0, GS, JU, AP), pp. 310–325.
- CADE-2017-FarberKU #monte carlo #proving
- Monte Carlo Tableau Proof Search (MF0, CK, JU), pp. 563–579.
- IJCAR-2018-PiotrowskiU #feedback #learning #named
- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (BP, JU), pp. 566–574.
- CADE-2019-BrownGKSU #challenge #named
- GRUNGE: A Grand Unified ATP Challenge (CEB, TG, CK, GS, JU), pp. 123–141.
- CADE-2019-ChvalovskyJ0U #named #performance
- ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E (KC, JJ, MS0, JU), pp. 197–215.