| [Urb05b] |
Josef Urban.
MoMM - fast interreduction and retrieval in large libraries of
formalized mathematics.
International Journal on Artificial Intelligence Tools, 2005.
forthcoming, available online at
http://ktiml.mff.cuni.cz/~urban/MoMM/momm.ps. [ bib | .ps ] |
| [Urb05a] |
Josef Urban.
MizarMode - an integrated proof assistance tool for the Mizar
way of formalizing mathematics.
Journal of Applied Logic, 2005.
forthcoming, available online at
http://ktiml.mff.cuni.cz/~urban/mizmode.ps. [ bib | .ps ] |
| [Urb05c] |
Josef Urban.
XML-izing Mizar: making semantic processing and presentation of
MML easy.
submitted to MKM 2005, available online at
http://ktiml.mff.cuni.cz/~urban/mizxml.ps, 2005. [ bib | .ps ] |
| [BU04] |
Grzegorz Bancerek and Josef Urban.
Integrated semantic browsing of the Mizar Mathematical Library
for authoring Mizar articles.
In Asperti et al. [ABT04], pages 44-57. [ bib | http ] |
| [ABT04] |
Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors.
Mathematical Knowledge Management, Third International
Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004,
Proceedings, volume 3119 of Lecture Notes in Computer Science.
Springer, 2004. [ bib ] |
| [Urb04] |
Josef Urban.
MPTP - motivation, implementation, first experiments.
Journal of Automated Reasoning, 33(3-4):319-339, 2004. [ bib | http ] |
| [Urb03b] |
Josef Urban.
Translating Mizar for first order theorem provers.
In MKM, volume 2594 of Lecture Notes in Computer Science,
pages 203-215. Springer, 2003. [ bib | http ] |
| [Urb03a] |
Josef Urban.
MPTP 0.1 - system description.
Electronic Notes in Theoretical Computer Science, 86(1), 2003. [ bib | .pdf ] |
| [Urb02c] |
Josef Urban.
Order sorted algebras.
Formalized Mathematics, 10(3):179-188, 2002. [ bib ] |
| [Urb02e] |
Josef Urban.
Subalgebras of an order sorted algebra. lattice of subalgebras.
Formalized Mathematics, 10(3):189-196, 2002. [ bib ] |
| [Urb02b] |
Josef Urban.
Homomorphisms of order sorted algebras.
Formalized Mathematics, 10(3):197-200, 2002. [ bib ] |
| [Urb02d] |
Josef Urban.
Order sorted quotient algebra.
Formalized Mathematics, 10(3):201-210, 2002. [ bib ] |
| [Urb02a] |
Josef Urban.
Free order sorted universal algebra.
Formalized Mathematics, 10(3):211-225, 2002. [ bib ] |
| [Urb01a] |
Josef Urban.
Basic facts about inaccessible and measurable cardinals.
Formalized Mathematics, 9(2):323-330, 2001. [ bib ] |
| [Urb01b] |
Josef Urban.
Mahlo and inaccessible cardinals.
Formalized Mathematics, 9(3):485-490, 2001. [ bib ] |
| [US99] |
Josef Urban and Petr Stepánek.
Experimenting with machine learning in automated theorem proving.
In Proceedings of the 8th Annual Conference of Doctoral Students
- WDS'99. MATFYZPRESS, 1999. [ bib ] |
Homomorphisms of Order Sorted Algebras
Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras
Mahlo and Inaccessible Cardinals
Basic Facts about Inaccessible and Measurable Cardinals
Translating Mizar for For First Order Theorem Provers
Libraries of Formalized Mathematics - Deductive AI Meets the Inductive AI
updated: 7. 1. 2005