Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Josef Urban's home page
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. The most suitable knowledge base currently
available for this purpose is in my opinion the formal
Mizar Mathematical Library.
That's one of the reasons why I am also quite involved in formalization and
computer-verification of mathematics (see the QEDManifesto),
especially in Mizar.