urban.bib

@COMMENT{{{This file has been generated by bib2bib 1.75}}

@COMMENT{{{Command line: /usr/bin/bib2bib -r -s year -c 'author : "Urban"' bib1.bib}}

@ARTICLE{Urban05-jait,
  AUTHOR = {Josef Urban},
  TITLE = {{M}o{M}{M} - Fast Interreduction and Retrieval in Large 
               Libraries of Formalized Mathematics.},
  JOURNAL = {International Journal on Artificial Intelligence Tools},
  YEAR = {2005},
  NOTE = {forthcoming, available online at http://ktiml.mff.cuni.cz/$\sim$urban/MoMM/momm.ps},
  URL = {http://ktiml.mff.cuni.cz/~urban/MoMM/momm.ps}
}

@ARTICLE{Urban05-jal,
  AUTHOR = {Josef Urban},
  TITLE = {{M}izar{M}ode - An Integrated Proof Assistance Tool for the 
               {M}izar Way of Formalizing Mathematics.},
  JOURNAL = {Journal of Applied Logic},
  EDITOR = {Christoph Benzmuller},
  YEAR = {2005},
  NOTE = {forthcoming, available online at http://ktiml.mff.cuni.cz/$\sim$urban/mizmode.ps},
  URL = {http://ktiml.mff.cuni.cz/~urban/mizmode.ps}
}

@UNPUBLISHED{Urban05-mkm,
  AUTHOR = {Josef Urban},
  TITLE = {{XML}-izing {M}izar: making semantic processing 
                  and presentation of {MML} easy},
  NOTE = {submitted to MKM 2005, available online at http://ktiml.mff.cuni.cz/$\sim$urban/mizxml.ps},
  YEAR = {2005},
  URL = {http://ktiml.mff.cuni.cz/~urban/mizxml.ps}
}

@INPROCEEDINGS{BancerekU04,
  AUTHOR = {Grzegorz Bancerek and
               Josef Urban},
  TITLE = {Integrated Semantic Browsing of the {M}izar {M}athematical {L}ibrary
               for Authoring {M}izar Articles.},
  BOOKTITLE = {MKM},
  YEAR = {2004},
  PAGES = {44-57},
  CROSSREF = {MKM2004},
  EE = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3119{\&}spage=44},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de},
  URL = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3119{\&}spage=44}
}

@PROCEEDINGS{MKM2004,
  EDITOR = {Andrea Asperti and
               Grzegorz Bancerek and
               Andrzej Trybulec},
  TITLE = {Mathematical Knowledge Management, Third International Conference,
               MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings},
  BOOKTITLE = {MKM},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {3119},
  YEAR = {2004},
  ISBN = {3-540-23029-7},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{Urban04-jar,
  AUTHOR = {Josef Urban},
  TITLE = {{M}{P}{T}{P} - Motivation, Implementation, First Experiments.},
  JOURNAL = {Journal of Automated Reasoning},
  VOLUME = {33},
  NUMBER = {3-4},
  YEAR = {2004},
  PAGES = {319-339},
  EE = {http://www.springerlink.com/index/10.1007/s10817-004-6245-1},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de},
  URL = {http://www.springerlink.com/index/10.1007/s10817-004-6245-1}
}

@INPROCEEDINGS{Urban03,
  AUTHOR = {Josef Urban},
  TITLE = {Translating {M}izar for First Order Theorem Provers.},
  BOOKTITLE = {MKM},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2594},
  YEAR = {2003},
  PAGES = {203-215},
  EE = {http://link.springer.de/link/service/series/0558/bibs/2594/25940203.htm},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de},
  URL = {http://link.springer.de/link/service/series/0558/bibs/2594/25940203.htm}
}

@ARTICLE{Urban03b,
  AUTHOR = {Josef Urban},
  TITLE = {{M}{P}{T}{P} 0.1 - System Description.},
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  VOLUME = {86},
  NUMBER = {1},
  YEAR = {2003},
  URL = {http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4DDWKNY-NH-1&_cdi=13109&_user=1490772&_orig=browse&_coverDate=05%2F31%2F2003&_sk=999139998&view=c&wchp=dGLbVlz-zSkzk&md5=891c8de092ce3ed335bac8dfebc01e66&ie=/sdarticle.pdf}
}

@ARTICLE{OSA-1,
  AUTHOR = {Josef Urban},
  TITLE = {Order sorted algebras},
  JOURNAL = {Formalized Mathematics},
  YEAR = {2002},
  VOLUME = {10},
  NUMBER = {3},
  PAGES = {179-188}
}

@ARTICLE{OSA-2,
  AUTHOR = {Josef Urban},
  TITLE = {Subalgebras of an order sorted algebra. Lattice of subalgebras},
  JOURNAL = {Formalized Mathematics},
  YEAR = {2002},
  VOLUME = {10},
  NUMBER = {3},
  PAGES = {189-196}
}

@ARTICLE{OSA-3,
  AUTHOR = {Josef Urban},
  TITLE = {Homomorphisms of order sorted algebras},
  JOURNAL = {Formalized Mathematics},
  YEAR = {2002},
  VOLUME = {10},
  NUMBER = {3},
  PAGES = {197-200}
}

@ARTICLE{OSA-4,
  AUTHOR = {Josef Urban},
  TITLE = {Order sorted quotient algebra},
  JOURNAL = {Formalized Mathematics},
  YEAR = {2002},
  VOLUME = {10},
  NUMBER = {3},
  PAGES = {201-210}
}

@ARTICLE{OSAFREE,
  AUTHOR = {Josef Urban},
  TITLE = {Free Order Sorted Universal Algebra},
  JOURNAL = {Formalized Mathematics},
  YEAR = {2002},
  VOLUME = {10},
  NUMBER = {3},
  PAGES = {211-225}
}

@ARTICLE{CARD-FIL,
  AUTHOR = {Josef Urban},
  TITLE = {Basic facts about inaccessible and measurable cardinals},
  JOURNAL = {Formalized Mathematics},
  YEAR = {2001},
  VOLUME = {9},
  NUMBER = {2},
  PAGES = {323-330}
}

@ARTICLE{CARD-LAR,
  AUTHOR = {Josef Urban},
  TITLE = {Mahlo and Inaccessible Cardinals},
  JOURNAL = {Formalized Mathematics},
  YEAR = {2001},
  VOLUME = {9},
  NUMBER = {3},
  PAGES = {485-490}
}

@INPROCEEDINGS{UrbanS99,
  AUTHOR = {Josef Urban and Petr {\v{S}}t\v{e}p\'{a}nek},
  TITLE = {Experimenting with Machine Learning in Automated Theorem Proving},
  BOOKTITLE = {Proceedings of the 8th Annual Conference of Doctoral Students - WDS'99},
  PUBLISHER = {MATFYZPRESS},
  YEAR = {1999}
}

This file has been generated by bibtex2html 1.75