I have moved to Prague, please see my updated webpage there.
I am a postdoc researcher in the Foundations Group of ICIS at the Radboud University, Nijmegen. Before that I was an assistant professor at the Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague (I co-founded the Prague Automated Reasoning Group), and a Marie-Curie fellow at the Department of Computer Science at University of Miami. (Short scientific CV)
Education
Ph.D. in Computer Science (2004),
Faculty of Mathematics and Physics,
Charles University, Prague
M.S. in Mathematics (1998),
Faculty of Mathematics and Physics,
Charles University, Prague
B.S. in Economics (1995),
Faculty of Social Sciences,
Charles University, Prague
Research Interests
I am interested in automated reasoning in large semantically
specified knowledge bases (some people call this "strong artificial
intelligence").
It involves automated deductive reasoning (automated theorem
proving), inductive reasoning (machine learning and discovery) and
their combining.
I am also quite involved in formalization and
computer-verification of mathematics (see the QED
Manifesto),
especially in Mizar.
Here is an interview,
a 2-page
paper (coming with
a talk
and slides)
and a longer paper
explaining what I have been doing for more than a decade and why. A lot of motivation is also in my earliest JAR paper about the first AI/ATP experiments done over Mizar in 2003.
Systems and Projects
-
Machine Learner for Automated Reasoning (MaLARea) (IJCAR'08 paper, CASC'13 results, CASC'12 results)
-
Automated Reasoning and Presentation Services for Mizar (MizAR) (JAR 2013 paper, Mizar 40 paper)
- HOL(y)Hammer: Learning-assisted Automated Reasoning for HOL Light (main paper, service description, 47% strengthening, lemmatization)
-
BliStr: The Blind Strategymaker (paper, slides)
-
Machine Learning Connection Prover (MaLeCoP) (the prototype is here)
-
Mizar Problems for Theorem Proving (MPTP) (JAR paper on 1st version, and JAR paper on 2nd version)
-
MoMM (Most of Mizar|Math Matches) (IJAIT paper)
-
Mizar mode for Emacs (JAL paper)
-
XML-based API to Mizar and transformations based on it (MKM paper)
-
E-MaLeS (Machine Learning of Strategies for E) (CADE'12 paper)
-
The Mizar-TPTP Semantic Presentation and Verification (SLGR paper)
-
Mizar Proof Advisor
-
Formal mathematics in a wiki (MathWiki)
-
Machine learning for automated reasoning (Learning2Reason)
-
Translation between Informal and Formal Mathematics (poster)
-
The MPTP $100 Challenges
- Formal articles on large cardinals: Basic Facts about Inaccessible and Measurable Cardinals, Mahlo and Inaccessible Cardinals
- Formal articles on order-sorted algebras: OSALG_1, OSALG_2, OSALG_3, OSALG_4, OSAFREE,
-
my GitHub (containing some more systems)
- Mizar TWiki
(from Chaos all things were born :-)
Contact details:
Grondslagen /
Intelligent Systems
ICIS /
FNWI,
Radboud Universiteit Nijmegen
Heijendaalseweg 135
6525 AJ Nijmegen
The Netherlands
e:
josef DOT urban AT
gmail DOT com
t: +31 24 365 26 31 (x52631 internally)
updated: 15. 12. 2013