@BOOK{MOST:1,
 AUTHOR={Mostowski, Andrzej},
 TITLE={Constructible Sets with Applications},
 PUBLISHER={North Holland},
 YEAR=1969}

@BOOK{BORSUK:1,
 AUTHOR={Borsuk, Karol and Szmielew, Wanda},
 TITLE={Foundations of Geometry},
 PUBLISHER={North Holland},
 YEAR=1960}

@ARTICLE{TARSKI:1,
 AUTHOR={Tarski, Alfred},
 TITLE={{\"U}ber unerreichbare {K}ardinalzahlen},
 JOURNAL={Fundamenta Mathematicae},
 YEAR=1938,
 VOLUME=30,
 PAGES={68--89}}

@ARTICLE{TARSKI:2,
 AUTHOR={Tarski, Alfred},
 TITLE={On Well-ordered Subsets of any Set},
 JOURNAL={Fundamenta Mathematicae},
 YEAR=1939,
 VOLUME=32,
 PAGES={176--183}}

@TECHREPORT{EDMONTON:89,
 AUTHOR={Rudnicki, Piotr and Trybulec, Andrzej},
 TITLE={A Collection of {\TeX ed} Mizar Abstracts},
 INSTITUTION={University of Alberta},
 YEAR=1989
 }

@BOOK{SZMIELEW:1,
  AUTHOR={Szmielew, Wanda},
  TITLE={From Affine to {E}uclidean Geometry},
  PUBLISHER={PWN -- D.Reidel Publ. Co.},
  YEAR=1983,
  VOLUME=27,
  ADDRESS={Warszawa -- Dordrecht}}

@ARTICLE{KUSAK:1,
  AUTHOR={Kusak, Eugeniusz},
  TITLE={A New Approach to Dimension-free Affine Geometry},
  JOURNAL={Bull. Acad. Polon. Sci. S{\'e}r. Sci. Math.},
  YEAR=1979,
  VOLUME=27,
  NUMBER={11--12},
  PAGES={875--882}}

@BOOK{KURAT:1,
  AUTHOR={Kuratowski, Kazimierz},
  TITLE={Wst{\c{e}}p do teorii mnogo{\'s}ci i topologii},
  PUBLISHER={PWN},
  YEAR=1977,
  ADDRESS={War\-sza\-wa}}

@BOOK{KURAT-MOST:1,
  AUTHOR={Kuratowski, Kazimierz and Mostowski, Andrzej},
  TITLE={Teoria mnogo{\'s}ci},
  PUBLISHER={PTM},
  YEAR=1952,
  ADDRESS={Wroc\-{\l}aw}}

@BOOK{KARGAP:1,
      AUTHOR = {Kargapo{\l}ow, M. I. and Mierzlakow, J. I.},
       TITLE = {Podstawy teorii grup},
   PUBLISHER = {PWN},
        YEAR = 1989,
     ADDRESS = {War\-sza\-wa}}

@BOOK{GUZ-ZBIER:1,
       AUTHOR = {Guzicki, Wojciech and Zbierski, Pawe{\l}},
        TITLE = {Podstawy teorii mnogo{\'s}ci},
    PUBLISHER = {PWN},
         YEAR = 1978,
      ADDRESS = {War\-sza\-wa}}

@BOOK{DIEUDONNE,
       AUTHOR = {Dieudonn{\'e}, Jean},
        TITLE = {Foundations of Modern Analysis},
    PUBLISHER = {Academic Press},
         YEAR = {1960},
      ADDRESS = {New York and London}}

@BOOK{MACKEY,
      AUTHOR = {Mackey, G.W.},
       TITLE = {The Mathematical Foundations of Quantum Mechanics},
   PUBLISHER = {North Holland},
        YEAR = {1963},
     ADDRESS = {New York, Amsterdam}}

@BOOK{Form.Math.1.1,
       TITLE = {Formalized {M}athematics: a computer assisted approach},
   PUBLISHER = {Universit{\'e} Catholique de Louvain},
        YEAR = {1990},
      VOLUME = {1({\bf 1})},
      NUMBER = {1},
       MONTH = {January}}

@ARTICLE{INTR.1.1,
      AUTHOR = {Trybulec, Andrzej},
       TITLE = {Introduction},
     JOURNAL = {Formalized {M}athematics},
   PUBLISHER = {Universit{\'e}  Catholique de Louvain},
        YEAR = {1990},
      VOLUME = {1({\bf 1})},
       MONTH = {January},
       PAGES = {7--8}}

@BOOK{Form.Math.1.2,
       TITLE = {Formalized {M}athematics: a computer assisted approach},
   PUBLISHER = {Universit{\'e}  Catholique de Louvain},
        YEAR = {1990},
      VOLUME = {1({\bf 2})},
      NUMBER = {2},
       MONTH = {March--April}}

@BOOK{Form.Math.2.1,
        TITLE = {Formalized {M}athematics: a computer assisted approach},
    PUBLISHER = {Universit{\'e}  Catholique de Louvain},
         YEAR = {1991},
       VOLUME = {2({\bf 1})},
       NUMBER = {1},
        MONTH = {January--February}}

@BOOK{Form.Math.2.4,
        TITLE = {Formalized {M}athematics: a computer assisted approach},
    PUBLISHER = {Universit{\'e}  Catholique de Louvain},
         YEAR = {1991},
       VOLUME = {2({\bf 4})},
       NUMBER = {4},
        MONTH = {September--October}}

@ARTICLE{POGORZELSKI.1975,
       AUTHOR = {Pogorzelski, Witold A. and Prucnal, Tadeusz},
        TITLE = {The Substitution Rule for Predicate Letters in the First-Order Predicate Calculus},
      JOURNAL = {Reports on Mathematical Logic},
         YEAR = {1975},
       NUMBER = {5},
        PAGES = {77--90}}

@BOOK{LUKA:1,
       AUTHOR = { {\L}ukasiewicz, Jan},
        TITLE = {Elementy logiki matematycznej},
    PUBLISHER = {PWN},
         YEAR = {1958},
      ADDRESS = {Warszawa}}

@BOOK{BORSUK:2,
       AUTHOR = {Borsuk, Karol},
        TITLE = {Theory of Shape},
    PUBLISHER = {PWN},
         YEAR = {1975},
       VOLUME = {59},
       SERIES = {Monografie Matematyczne},
      ADDRESS = {Warsaw}}

@ARTICLE{BORSUK:3,
       AUTHOR = {Borsuk, Karol},
        TITLE = {On the Homotopy Types of Some Decomposition Spaces},
      JOURNAL = {Bull. Acad. Polon. Sci.},
         YEAR = {1970},
       NUMBER = {18},
        PAGES = {235--239}}

@BOOK{SIKORSKI:1,
       AUTHOR = {Sikorski, R.},
        TITLE = {Rachunek r{\'o}{\.z}niczkowy i ca{\l}kowy -- funkcje wielu zmiennych},
    PUBLISHER = {PWN - Warszawa},
       SERIES = {Biblioteka Matematyczna},
         YEAR = {1968}}

@BOOK{GRZEG1,
       AUTHOR = {Grzegorczyk, Andrzej},
        TITLE = {Zarys logiki matematycznej},
    PUBLISHER = {PWN},
         YEAR = {1973},
      ADDRESS = {Warsaw}}

@BOOK{Wilson,
       AUTHOR = { Wilson, Robin},
        TITLE = { Wprowadzenie do teorii graf{\'o}w},
    PUBLISHER = { PWN},
         YEAR = { 1985}}

@ARTICLE{LAMBEK:1,
       AUTHOR = {Lambek, Joachim},
        TITLE = {The Mathematics of Sentence Structure},
      JOURNAL = {American Mathematical Monthly},
         YEAR = {1958},
       NUMBER = {65},
        PAGES = {154--170}}

@BOOK{MacLane:1,
       AUTHOR = {Mac Lane, Saunders},
        TITLE = {Categories  for the Working Mathematician},
    PUBLISHER = {Springer Verlag},
         YEAR = {1971},
       VOLUME = {5},
       SERIES = {Graduate Texts in Mathematics},
      ADDRESS = {New York, Heidelberg, Berlin}}

@BOOK{BOURBAKI,
       AUTHOR = {Bourbaki, Nicolas},
        TITLE = {Elements de Mathematique},
    PUBLISHER = {HERMANN},
         YEAR = {1960},
       VOLUME = {Topologie Generale},
      EDITION = {Troisieme edition}}

@BOOK{MUZALEWSKI:1,
       AUTHOR = {Muzalewski, Micha{\l}},
        TITLE = {Foundations of {M}etric-{A}ffine {G}eometry},
    PUBLISHER = {Dzia{\l} {W}ydawnictw {F}ilii {U}{W} w {B}ia{\l}ymstoku},
      ADDRESS = {Filia {UW} w Bia{\l}ymstoku},
         YEAR = {1990}}

@BOOK{SEMAD,
       AUTHOR = {Semadeni, Zbigniew and Wiweger, Antoni},
        TITLE = {Wst{\c e}p do teorii kategorii i funktor{\'o}w},
    PUBLISHER = {PWN},
         YEAR = {1978},
       VOLUME = {45},
       SERIES = {Biblioteka Matematyczna},
      ADDRESS = {Warszawa}}

@BOOK{KELL55,
       AUTHOR = {Kelley, John L.},
        TITLE = {General Topology},
    PUBLISHER = {von Nostrand},
         YEAR = {1955},
       VOLUME = {I,II}}

@BOOK{KURAT:2,
       AUTHOR = {Kuratowski, Kazimierz},
        TITLE = {Topology},
    PUBLISHER = {PWN -- Polish Scientific Publishers, Academic Press},
         YEAR = {1966},
       VOLUME = {I},
      ADDRESS = {Warsaw, New York and London}}

@BOOK{RASIOWA-SIKOR,
       AUTHOR = {Rasiowa, Helena and Sikorski, Roman},
        TITLE = {The {M}athematics of {M}etamathematics},
    PUBLISHER = {PWN},
         YEAR = {1968},
       VOLUME = {41},
       SERIES = {Monografie Matematyczne},
      ADDRESS = {Warszawa}}

@BOOK{TRACZYK,
       AUTHOR = {Traczyk, Tadeusz},
        TITLE = {Wst{\c e}p do teorii algebr {B}oole'a},
    PUBLISHER = {PWN},
         YEAR = {1970},
       VOLUME = {37},
       SERIES = {Biblioteka Matematyczna},
      ADDRESS = {Warszawa}}

@BOOK{HUNGERFORD,
       AUTHOR = {Hungerford, Thomas W.},
        TITLE = {Algebra},
    PUBLISHER = {Springer-Verlag New York Inc.},
         YEAR = {1974},
       VOLUME = {73},
       SERIES = {Graduate Texts in Mathematics},
      ADDRESS = {Seattle, Washington USA},
      EDITION = {{D}epartment of {M}athematics {U}niversity of {W}ashington}}

@BOOK{Lang,
       AUTHOR = {Lang, Serge},
        TITLE = {Algebra},
    PUBLISHER = {PWN},
         YEAR = {1984},
      ADDRESS = {Warszawa}}

@BOOK{POGO:1,
       AUTHOR = {Pogorzelski, Witold A.},
        TITLE = {Klasyczny Rachunek Predykat\' ow},
    PUBLISHER = {PWN},
         YEAR = {1981},
      ADDRESS = {Warszawa}}

@ARTICLE{POGO:2,
       AUTHOR = {Lesisz, W{\l}odzimierz and Pogorzelski, Witold A.},
        TITLE = {A Simplified Definition of the Notion of Similarity between Formulas of the First Order Predicate Calculus},
      JOURNAL = {Reports on Mathematical Logic},
         YEAR = {1976},
       NUMBER = {7},
        PAGES = {63--69}}

@BOOK{BIRKHOFF:1,
       AUTHOR = {Birkhoff, Garrett},
        TITLE = {Lattice Theory},
    PUBLISHER = {Providence, Rhode Island},
         YEAR = {1967},
      ADDRESS = {New York}}

@ARTICLE{ISOMICHI,
       AUTHOR = {Isomichi, Yoshinori},
        TITLE = {New Concepts in the Theory of Topological Space -- Supercondensed Set, Subcondensed Set, and Condensed Set},
      JOURNAL = {Pacific Journal of Mathematics},
         YEAR = {1971},
       VOLUME = {38},
       NUMBER = {3},
        PAGES = {657--668}}

@BOOK{MOST-KURAT:3,
       AUTHOR = {Kuratowski, Kazimierz and Mostowski, Andrzej},
        TITLE = {Set Theory (with an introduction to descriptive set theory)},
    PUBLISHER = {PWN -- Polish Scientific Publishers and North-Holland Publishing Company},
         YEAR = {1976},
       VOLUME = {86},
       SERIES = {Studies in Logic and The Foundations of Mathematics},
      ADDRESS = {Warsaw-Amsterdam}}

@ARTICLE{KURAT:4,
       AUTHOR = {Kuratowski, Kazimierz},
        TITLE = {Sur l'op\'{e}ration $\overline{A}$ de l'Analysis Situs},
      JOURNAL = {Fundamenta Mathematicae},
         YEAR = {1922},
       VOLUME = {3},
        PAGES = {182--199}}

@BOOK{ENGEL:1,
       AUTHOR = {Engelking, Ryszard},
        TITLE = {General Topology},
    PUBLISHER = {PWN -- Polish Scientific Publishers},
         YEAR = {1977},
       VOLUME = {60},
       SERIES = {Monografie Matematyczne},
      ADDRESS = {Warsaw}}

@BOOK{CECH:1,
       AUTHOR = { \v{C}ech, Eduard},
        TITLE = {Topological Spaces},
    PUBLISHER = {Academia, Publishing House of the Czechoslovak Academy of Sciences},
         YEAR = {1966},
      ADDRESS = {Prague}}

@BOOK{BROWN:1,
       AUTHOR = {Brown, Robert H.},
        TITLE = {The {L}efschetz Fixed Point Theorem},
    PUBLISHER = {Scott--Foresman},
         YEAR = {1971},
      ADDRESS = {New York}}

@BOOK{DUG-GRAN:1,
       AUTHOR = {Dugundji, James and Granas, Andrzej},
        TITLE = {Fixed Point Theory},
    PUBLISHER = {PWN -- Polish Scientific Publishers},
         YEAR = {1982},
       VOLUME = {I},
      ADDRESS = {Warsaw}}

@ARTICLE{BROUWER:1,
       AUTHOR = {Brouwer, L.},
        TITLE = {{\"U}ber {A}bbildungen von {M}annigfaltigkeiten},
      JOURNAL = {Mathematische Annalen},
         YEAR = {1912},
       VOLUME = {38},
       NUMBER = {71},
        PAGES = {97--115}}

@ARTICLE{STONE:1,
       AUTHOR = {Stone, M. H.},
        TITLE = {Algebraic Characterizations of Special {B}oolean Rings},
      JOURNAL = {Fundamenta Mathematicae},
         YEAR = {1937},
       VOLUME = {29},
        PAGES = {223--303}}

@TECHREPORT{TAKE-NAKA,
       AUTHOR = {Takeuchi, Yukio and Nakamura, Yatsuka},
        TITLE = {On the {J}ordan curve theorem},
  INSTITUTION = {Dept. of Information Eng., Shinshu University},
         YEAR = {1980},
       NUMBER = {19804},
      ADDRESS = {500 Wakasato, Nagano city, Japan},
        MONTH = {April}}

@TECHREPORT{On,
       AUTHOR = {Takeuchi, Yukio and Nakamura, Yatsuka},
        TITLE = {On the {J}ordan curve theorem},
  INSTITUTION = {Dept. of Information Eng., Shinshu University},
         YEAR = {1980},
       NUMBER = {19804},
      ADDRESS = {500 Wakasato, Nagano city, Japan},
        MONTH = {April}}

@BOOK{PATKOWSKA:74,
       AUTHOR = {Patkowska, Hanna},
        TITLE = {Wst{\c e}p do Topologii},
    PUBLISHER = {PWN},
         YEAR = {1974},
      ADDRESS = {Warszawa}}

@ARTICLE{STONE:2,
       AUTHOR = {Stone, A. H.},
        TITLE = {Paracompactness and Product Spaces},
      JOURNAL = {Bull. Amer. Math. Soc.},
         YEAR = {1948},
       VOLUME = {54},
        PAGES = {977--982}}

@ARTICLE{RUDIN:1,
       AUTHOR = {Rudin, M. E.},
        TITLE = {A new proof that metric spaces are paracompact},
      JOURNAL = {Proc. Amer. Math. Soc.},
         YEAR = {1969},
       VOLUME = {20},
        PAGES = {603}}

@BOOK{Dick,
       AUTHOR = {Dick, Wick Hall and Guilford, L.Spencer {II}},
        TITLE = {Elementary Topology},
    PUBLISHER = {John Wiley \& Sons Inc.},
         YEAR = {1955}}

@TECHREPORT{NAKAMURA1,
       AUTHOR = {Nakamura, Yatsuka},
        TITLE = {On a Mathematical Model of {CPU} and Algorithm},
  INSTITUTION = {Shinshu University},
         YEAR = {1991},
        MONTH = {Aug}}

@ARTICLE{ELGOT-ROBIN,
       AUTHOR = {Elgot, C.C. and Robinson, A.},
        TITLE = {Random Access Stored-Program Machines, an Approach to Programming Languages},
      JOURNAL = {J.A.C.M.},
         YEAR = {1964},
       VOLUME = {11},
       NUMBER = {4},
        PAGES = {365--399},
        MONTH = {Oct}}

@INPROCEEDINGS{Nakamura:2,
       AUTHOR = {Nakamura, Yatsuka},
        TITLE = {Finite Topology Concept for Discrete Spaces},
    BOOKTITLE = {Proceedings of the Eleventh Symposium on Applied Functional Analysis},
         YEAR = {1988},
       EDITOR = {H.~Umegaki},
        PAGES = {111--116},
 ORGANIZATION = {Science University of Tokyo},
      ADDRESS = {Noda-City, Chiba, Japan}}

@ARTICLE{Nakamura:3,
       AUTHOR = {Nakamura, Yatsuka and Fuwa, Yasushi and Imura, Hiroshi},
        TITLE = {A Theory of Finite Topology and Image Processing},
      JOURNAL = {Journal of the Faculty of Engineering, Shinshu University},
         YEAR = {1991},
       NUMBER = {69},
        PAGES = {11--24},
        MONTH = {Sep.}}

@INPROCEEDINGS{Nakamura:4,
       AUTHOR = {Kawamoto, Pauline N. and Eguchi, Masayoshi and Fuwa, Yasushi and Nakamura, Yatsuka},
        TITLE = {Deadlocks\Traps which Result from the Order-Dependence of {P}etri Net Transitions},
    BOOKTITLE = {Shinetsu Shibu Conv. Rec.},
         YEAR = {1992},
        PAGES = {345-346},
 ORGANIZATION = {IEICE},
        MONTH = {Oct}}

@BOOK{SZABO,
       AUTHOR = {Szabo, M. E.},
        TITLE = {Algebra of Proofs},
    PUBLISHER = {North Holland},
         YEAR = 1978}

@BOOK{KURAT:3,
       AUTHOR = {Kuratowski, Kazimierz},
        TITLE = {Topology},
    PUBLISHER = {PWN -- Polish Scientific Publishers, Academic Press},
         YEAR = {1968},
       VOLUME = {II},
      ADDRESS = {Warsaw, New York and London}}

@INPROCEEDINGS{Nakamura:5,
       AUTHOR = {Kawamoto, Pauline N. and Eguchi, Masayoshi and Fuwa, Yasushi and Nakamura, Yatsuka},
        TITLE = {The Detection of Deadlocks in {P}etri Nets with Ordered Evaluation Sequences},
    BOOKTITLE = {Institute of Electronics, Information, and Communication Engineers (IEICE) Technical Report},
         YEAR = {1993},
        PAGES = {45-52},
 ORGANIZATION = {Institute of Electronics, Information, and Communication Engineers (IEICE)},
        MONTH = {January},
         NOTE = {}}

@BOOK{SIKORSKI:2,
       AUTHOR = {Sikorski, Roman},
        TITLE = {Boolean Algebras},
    PUBLISHER = {Springer-Verlag},
         YEAR = {1960},
       VOLUME = {25},
       SERIES = {Ergebnisse der Mathematik und ihrer Grenzgebiete},
         NOTE = {}}

@BOOK{DIJKSTRA,
       AUTHOR = {Dijkstra, Edsger W.},
        TITLE = {Selected Writings on Computing, a Personal Perspective}}

@ARTICLE{STONE:3,
       AUTHOR = {Stone, M. H.},
        TITLE = {Application of {B}oolean algebras to topology},
      JOURNAL = {Math. Sb.},
         YEAR = {1936},
       VOLUME = {1},
        PAGES = {765--771}}

@ARTICLE{Tar-Wir1,
       AUTHOR = {Tarlecki, Andrzej and Wirsing, Martin},
        TITLE = {Continuous Abstract Data Types},
      JOURNAL = {Fundamenta Informaticae},
       SERIES = {Annales Societatis Mathematicae Polonae},
         YEAR = {1986},
       VOLUME = {9},
       NUMBER = {1},
        PAGES = {95--125}}

@BOOK{ALEX-HOPF,
       AUTHOR = {Alexandroff, P. and Hopf, H. H.},
        TITLE = {Topologie {I}},
    PUBLISHER = {Springer-Verlag},
         YEAR = {1935},
      ADDRESS = {Berlin}}

@BOOK{THRON:1,
       AUTHOR = {Thron, W.J.},
        TITLE = {Topological Structures},
    PUBLISHER = {Holt, Rinehart and Winston},
         YEAR = {1966},
      ADDRESS = {New York}}

@ARTICLE{WARREN:1,
       AUTHOR = {Warren, R.H.},
        TITLE = {Identification spaces and unique uniformity},
      JOURNAL = {Pacific Journal of Mathematics},
         YEAR = {1981},
       VOLUME = {95},
        PAGES = {483--492}}

@ARTICLE{GIRARD:TCS50,
       AUTHOR = {Girard, J.-Y.},
        TITLE = {Linear Logic},
      JOURNAL = {Theoretical Computer Science},
         YEAR = {1987},
       VOLUME = {50},
       NUMBER = {1},
        PAGES = {1--102}}

@ARTICLE{YETTER,
       AUTHOR = {Yetter, Davide N.},
        TITLE = {Quantales and (Noncommutative) Linear Logic},
      JOURNAL = {The Journal of Symbolic Logic},
         YEAR = {1990},
       VOLUME = {55},
       NUMBER = {1},
        PAGES = {41--64},
        MONTH = {March}}

@ARTICLE{BLIKLE,
       AUTHOR = {Blikle, A.},
        TITLE = {An Analysis of Programs by Algebraic Means},
      JOURNAL = {Banach Center Publications},
       VOLUME = {2},
        PAGES = {167--213}}

@BOOK{ddq,
       AUTHOR = {Denning, P. J. and Dennis, J. B. and Qualitz, J. E.},
        TITLE = {Machines, Languages, and Computation},
    PUBLISHER = {Prentice-Hall},
         YEAR = {1978}}

@BOOK{BALCERZYK,
       AUTHOR = {Balcerzyk, Stanis{\l}aw},
        TITLE = {Wst\c{e}p do algebry homologicznej},
    PUBLISHER = {PWN},
         YEAR = {1972},
       VOLUME = {34},
       SERIES = {Biblioteka Matematyczna},
      ADDRESS = {Warszawa}}

@ARTICLE{TarleckiBurstallGoguen,
       AUTHOR = {Tarlecki, Andrzej and Burstall, Rod M. and Goguen, Joseph, A.},
        TITLE = {Some fundamental algebraic tools for the semantics of computation: {P}art 3. {I}ndexed categories},
      JOURNAL = {Theoretical Computer Science},
         YEAR = {1991},
       VOLUME = {91},
        PAGES = {239--264}}

@ARTICLE{GoguenBurstall,
       AUTHOR = {Goguen, Joseph A. and Burstall, Rod M.},
        TITLE = {Introducing institutions},
      JOURNAL = {Lecture Notes in Computer Science},
         YEAR = {1984},
       VOLUME = {164},
        PAGES = {221--256}}

@ARTICLE{BachmairDershowitz,
       AUTHOR = {Bachmair, Leo and Dershowitz, Nachum},
        TITLE = {Critical Pair Criteria for Completion},
      JOURNAL = {Journal of Symbolic Computation},
         YEAR = {1988},
       VOLUME = {6},
       NUMBER = {1},
        PAGES = {1--18}}

@ARTICLE{KlopMiddeldorp,
       AUTHOR = {Klop, Jan Willem and Middeldorp, Aart},
        TITLE = {An Introduction to {K}nuth-{B}endix Completion},
      JOURNAL = {CWI Quarterly},
         YEAR = {1988},
       VOLUME = {1},
       NUMBER = {3},
        PAGES = {31--52}}

@INPROCEEDINGS{KnuthBendix,
       AUTHOR = {Knuth, Donald E. and Bendix, Peter B.},
        TITLE = {Simple word problems in universal algebras.},
    BOOKTITLE = {Computational Problems in Abstract Algebras},
         YEAR = {1970},
       EDITOR = {J. Leech},
        PAGES = {263--297},
    PUBLISHER = {Pergamon},
      ADDRESS = {Oxford}}

@BOOK{HofLinCS,
       EDITOR = {Abramsky, S. and Gabbay, D.~M. and Maibaum, S.~E.},
        TITLE = {Handbook of Logic in Computer Science, vol.~2: {C}omputational structures},
    PUBLISHER = {Clarendon Press},
         YEAR = {1992},
      ADDRESS = {Oxford}}

@BOOK{WECHLER,
       AUTHOR = {Wechler, Wolfgang},
        TITLE = {Universal Algebra for Computer Scientists},
    PUBLISHER = {Springer--Verlag},
         YEAR = {1992},
       VOLUME = {25},
       SERIES = {EATCS Monographs on TCS}}

@ARTICLE{Huet81,
       AUTHOR = {Huet, Gerard},
        TITLE = {A Complete Proof of Correctness of the {K}nuth-{B}endix Completion},
      JOURNAL = {Journal of Computer and System Sciences},
         YEAR = {1981},
       VOLUME = {23},
       NUMBER = {1},
        PAGES = {3--57}}

@BOOK{CCL,
       AUTHOR = {Gierz, G. and Hofmann, K.H. and Keimel, K. and Lawson, J.D. and Mislove, M. and Scott, D.S.},
        TITLE = {A Compendium of Continuous Lattices},
    PUBLISHER = {Springer-Verlag},
         YEAR = {1980},
      ADDRESS = {Berlin, Heidelberg, New York}}

@BOOK{Johnstone,
       AUTHOR = {Johnstone, Peter T.},
        TITLE = {{S}tone Spaces},
    PUBLISHER = {Cambridge University Press},
         YEAR = {1982},
      ADDRESS = {Cambridge, London, New York}}

@ARTICLE{lns82,
       AUTHOR = {Lassez, J.-L. and Nguyen, V. L. and Sonenberg, E. A},
        TITLE = {Fixed Point Theorems and Semantics: a folk tale},
      JOURNAL = {Information Processing Letters},
         YEAR = {1982},
       VOLUME = {14},
       NUMBER = {3},
        PAGES = {112--116}}

@ARTICLE{lcp95,
       AUTHOR = {Paulson, Lawrence C.},
        TITLE = {Set Theory for Verification: {II}, Induction and Recursion},
      JOURNAL = {Journal of Automated Reasoning},
         YEAR = {1995},
       VOLUME = {15},
       NUMBER = {2},
        PAGES = {167--215}}

@ARTICLE{abi68,
       AUTHOR = {Abian, A.},
        TITLE = {A fixed point theorem},
      JOURNAL = {Nieuw Arch. Wisk.},
         YEAR = {1968},
       VOLUME = {3},
       NUMBER = {16},
        PAGES = {184--185}}

@ARTICLE{maw69,
       AUTHOR = {M{\Pla}kowski, A. and Wi\'sniewski, K.},
        TITLE = {{G}eneralization of {A}bian's fixed point theorem},
      JOURNAL = {Annales Soc. Math. Pol. Series I},
         YEAR = {1969},
       VOLUME = {XIII},
        PAGES = {63--65}}

@BOOK{mgm,
       AUTHOR = {Murdeshwar, M.G.},
        TITLE = {General Topology},
    PUBLISHER = {Wiley Eastern},
         YEAR = {1990}}

@BOOK{takagi,
       AUTHOR = {Takagi, Teiji},
        TITLE = {Elementary Theory of Numbers},
    PUBLISHER = {Kyoritsu Publishing Co., Ltd.},
         YEAR = {1995},
      EDITION = {Second}}

@BOOK{shilov,
       EDITOR = {Shilov, Georgi E.},
        TITLE = {Elementary Real and Complex Analysis (English translation,
                 translated by {R}ichard {A}. {S}ilverman)},
    PUBLISHER = {The MIT Press},
         YEAR = {1973}}

@INPROCEEDINGS{tor96,
       AUTHOR = {Franzen, T.},
        TITLE = {Teaching mathematics through formalism: a few caveats},
    BOOKTITLE = {Proceedings of the {DIMACS} {S}ymposium on {T}eaching {L}ogic},
         YEAR = {1996},
       EDITOR = {D.~Gries},
 ORGANIZATION = {DIMACS},
         NOTE = { \\ On WWW: {\tt http://dimacs.rutgers.edu/Workshops/Logic/program.html}
}}

@BOOK{Greenberg,
       AUTHOR = {Greenberg, Marvin J.},
        TITLE = {Lectures on Algebraic Topology},
    PUBLISHER = {W.~A.~Benjamin, Inc.},
         YEAR = {1973}}

@BOOK{GanterWille,
       AUTHOR = {Ganter, Bernhard and Wille, Rudolf},
        TITLE = {Formal Concept Analysis},
    PUBLISHER = {Springer Verlag, Berlin, Heidelberg, New York},
         YEAR = {1996},
         NOTE = {(written in German)}}

@BOOK{Ribenboim,
       AUTHOR = {Ribenboim, Paulo},
        TITLE = {The World of Prime Numbers},
    PUBLISHER = {Kyoritsu Publishing Co., Ltd.},
         YEAR = {1995},
      EDITION = {Second}}

@BOOK{BraBra96,
       AUTHOR = {Brassard, Gilles and Bratley, Paul},
        TITLE = {Fundamentals of Algorithmics},
    PUBLISHER = {Prentice Hall},
         YEAR = {1996}}

@BOOK{Gratzer,
       AUTHOR = {Gr\"atzer, George},
        TITLE = {General Lattice Theory},
    PUBLISHER = {Academic Press, New York},
         YEAR = {1978}}

@BOOK{Becker93,
       author = {Becker, Thomas and Weispfenning, Volker},
	title = {Gr\"{o}bner Bases: A Computational Approach
                to Commutative Algebra},
         year = {1993},
    publisher = {Springer-Verlag, New York, Berlin}}

@BOOK{MatTry77,
       AUTHOR = {Matuszewski, Roman and Trybulec, Andrzej},
        TITLE = {Certain algorithm of classification in metric spaces},
    PUBLISHER = {Warsaw University, Bialystok Campus},
         YEAR = {1977},
       VOLUME = {V, Number 20},
       SERIES = {Mathematical Papers}}

@BOOK{Uspenski60,
       AUTHOR = {Uspenskii, V. A.},
        TITLE = {Lektsii o vychislimykh funktsiakh},
    PUBLISHER = {Gos. Izd. Phys.-Math. Lit., Moskva},
         YEAR = {1960}}

@ARTICLE{Huntington1,
       AUTHOR = {Huntington, E.~V.},
        TITLE = {Sets of independent postulates for the algebra of logic},
      JOURNAL = {Trans. AMS},
         YEAR = {1904},
       VOLUME = {5},
        PAGES = {288--309}}

@ARTICLE{Huntington2,
       AUTHOR = {Huntington, E.~V.},
        TITLE = {New sets of independent postulates
                 for the algebra of logic, with special
                 reference to {W}hitehead and {R}ussell's
                 {P}rincipia {M}athematica},
      JOURNAL = {Trans. AMS},
         YEAR = {1933},
       VOLUME = {35},
        PAGES = {274--304}}

@ARTICLE{Huntington3,
       AUTHOR = {Huntington, E.~V.},
        TITLE = {Boolean algebra. {A} correction},
      JOURNAL = {Trans. AMS},
         YEAR = {1933},
       VOLUME = {35},
        PAGES = {557--558}}

@ARTICLE{McCuneRob,
       AUTHOR = {McCune, W.},
        TITLE = {Solution of the {R}obbins problem},
      JOURNAL = {Journal of Automated Reasoning},
         YEAR = {1997},
       VOLUME = {19},
        PAGES = {263--276}}

@ARTICLE{DahnRob,
       AUTHOR = {Dahn, B.~I.},
        TITLE = {Robbins algebras are {B}oolean: A revision of {M}c{C}une's
                computer-generated solution of {R}obbins problem},
      JOURNAL = {Journal of Algebra},
         YEAR = {1998},
       VOLUME = {208},
        PAGES = {526--532}}

@BOOK{arm74,
       AUTHOR = {Armstrong, W.~W.},
        TITLE = {Dependency {S}tructures of {D}ata {B}ase {R}elationships},
    PUBLISHER = {Information Processing 74, North Holland},
         YEAR = {1974}}

@BOOK{SLang,
       AUTHOR = {Lang, Serge},
        TITLE = {Algebra},
    PUBLISHER = {Addison-Wesley},
         YEAR = {1980}}

@BOOK{RUDIN:2,
       AUTHOR = {Rudin, Walter},
        TITLE = {Real and Complex Analysis},
    PUBLISHER = {Mc Graw-Hill, Inc.},
         YEAR = {1974}}

@BOOK{Maurin,
       AUTHOR = {Maurin, Krzysztof},
        TITLE = {Analiza, {II}},
    PUBLISHER = {PWN -- Warszawa},
       SERIES = {Biblioteka Matematyczna},
       VOLUME = {70},
         YEAR = {1991}}

@ARTICLE{Thomasse,
       AUTHOR = {Thomasse, Stephan},
        TITLE = {On Better-quasi-ordering Countable Series-parallel Orders},
      JOURNAL = {Transactions of the American Mathematical Society},
         YEAR = {2000},
       VOLUME = {352(6)},
        PAGES = {2491--2505}}

@ARTICLE{Gallai,
       AUTHOR = {Gallai, Tibor},
        TITLE = {Transitiv Orientierbare Graphen},
      JOURNAL = {Acta Math. Acad. Sci. Hungar.},
         YEAR = {1967},
       VOLUME = {18},
        PAGES = {25--66}}

@BOOK{Chagrov,
       AUTHOR = {Chagrov, A. and Zakharyaschev, M.},
        TITLE = {Modal Logic},
    PUBLISHER = {Clarendon Press, Oxford},
         YEAR = {1997}}

@BOOK{Newman51,
       AUTHOR = {Newman, M.~H.~A.},
        TITLE = {Elements of the Topology of Plane Sets of Points},
    PUBLISHER = {Cambridge University Press},
         YEAR = {1951}}

@ARTICLE{Dijkstra59,
       AUTHOR = {Dijkstra, E.~W.},
        TITLE = {A Note on Two Problems in Connection with Graphs},
      JOURNAL = {Numer. Math.},
         YEAR = {1959},
       VOLUME = {1},
        PAGES = {269--271}}

@BOOK{Halmos87,
       AUTHOR = {Halmos, P.~R.},
        TITLE = {Introduction to {H}ilbert Space},
    PUBLISHER = {American Mathematical Society},
         YEAR = {1987}}

@BOOK{Elmasri,
       AUTHOR = {Elmasri, Ramez and Navathe, Shamkant B.},
        TITLE = {Fundamentals of Database Systems},
    PUBLISHER = {Addison-Wesley},
         YEAR = {2000}}

@BOOK{Maier,
       AUTHOR = {Maier, David},
        TITLE = {The Theory of Relational Databases},
    PUBLISHER = {Computer Science Press, Rockville},
         YEAR = {1983}}

@BOOK{Csaszar,
       AUTHOR = {Csaszar, Akos},
        TITLE = {General Topology},
    PUBLISHER = {Akademiai Kiado, Budapest},
         YEAR = {1978}}

@ARTICLE{McCune:2001,
       AUTHOR = {McCune, W. and Veroff, R. and Fitelson, B.
                 and Harris, K. and Feist, A. and Wos, L.},
        TITLE = {Short Single Axioms for {B}oolean Algebra},
      JOURNAL = {Journal of Automated Reasoning},
         YEAR = {2002},
       VOLUME = {29(1)},
        PAGES = {1--16}}

@ARTICLE{Meredith:1968,
       AUTHOR = {Meredith, C.~A. and Prior, A.~N.},
        TITLE = {Equational Logic},
      JOURNAL = {Notre Dame Journal of Formal Logic},
         YEAR = {1968},
       VOLUME = {9},
        PAGES = {212--226}}

@INPROCEEDINGS{Bancerek:2003,
         AUTHOR = {Bancerek, Grzegorz},
          TITLE = {On the Structure of {M}izar Types},
      BOOKTITLE = {Electronic Notes in Theoretical Computer Science},
           YEAR = {2003},
         VOLUME = {85},
          ISSUE = {7},
      PUBLISHER = {Elsevier},
         EDITOR = {Herman Geuvers and Fairouz Kamareddine}}

@BOOK{RockTyr:1970,
       AUTHOR = {Rockafellar, Tyrrell R.},
        TITLE = {Convex Analysis},
    PUBLISHER = {Princeton University Press},
         YEAR = {1970}}

@ARTICLE{Wronski:1974,
       AUTHOR = {Wro{\'n}ski, Andrzej},
        TITLE = {Remarks on Intermediate Logics with Axioms
                Containing Only One Variable},
      JOURNAL = {Reports on Mathematical Logic},
         YEAR = {1974},
       VOLUME = {2},
        PAGES = {63--76}}

@BOOK{Hall:1959,
       AUTHOR = {Hall Jr., Marshall},
        TITLE = {The Theory of Groups},
    PUBLISHER = {The Macmillan Company, New York},
         YEAR = {1959}}

@ARTICLE{Hall:1935,
       AUTHOR = {Hall, Philip},
        TITLE = {On Representatives of Subsets},
      JOURNAL = {Journal of London Mathematical Society},
         YEAR = {1935},
       VOLUME = {10},
        PAGES = {26--30}}

@ARTICLE{Sheffer:1913,
    AUTHOR = {Sheffer, Henry Maurice},
     TITLE = {A Set of Five Independent Postulates
              for {B}oolean Algebras, with Application to Logical Constants},
   JOURNAL = {Transactions of American Mathematical Society},
    VOLUME = {14},
    NUMBER = {4},
     PAGES = {481--488},
      YEAR = {1913}}

@ARTICLE{Yabuta:01,
    AUTHOR = {Yabuta, Minoru},
     TITLE = {A Simple Proof
              of {C}armichael's Theorem of Primitive Divisors},
   JOURNAL = {The Fibonacci Quarterly},
    VOLUME = {39},
    NUMBER = {5},
     PAGES = {439--443},
      YEAR = {2001}}

@ARTICLE{ANKPJG,
    AUTHOR = {Naumowicz, Adam and Pra\.zmowski, Krzysztof},
     TITLE = {On {S}egre's Product of Partial Line Spaces and Spaces of Pencils},
   JOURNAL = {Journal of Geometry},
    VOLUME = {71},
    NUMBER = {{\bf 1}},
     PAGES = {128--143},
      YEAR = {2001}}

@ARTICLE{ANKPRM,
    AUTHOR = {Naumowicz, Adam and Pra\.zmowski, Krzysztof},
     TITLE = {The Geometry of Generalized {V}eronese Spaces},
   JOURNAL = {Results in Mathematics},
    VOLUME = {45},
     PAGES = {115--136},
      YEAR = {2004}}

@ARTICLE{Riguet,
       AUTHOR = {Riguet, Jacques},
        TITLE = {Relations binaires, fermetures, correspondances de {G}alois},
      JOURNAL = {Bulletin de la S.M.F.},
         YEAR = {1948},
       VOLUME = {76},
        PAGES = {114--155},
         NOTE = {On WWW: {\tt http://www.numdam.org/item?id=\-BSFM\_1948\_\_76\_\_114\_0}}}

@ARTICLE{McCune:2005,
       AUTHOR = {McCune, W. and Padmanabhan, R. and Rose, M. A. and Veroff, R.},
        TITLE = {Automated Discovery of Single Axioms for Ortholattices},
      JOURNAL = {Algebra Universalis},
         YEAR = {2005},
       VOLUME = {52(4)},
        PAGES = {541--549}}

@BOOK{gl04,
       AUTHOR = {Lee, Gilbert},
        TITLE = {Verification of graph algorithms in {M}izar},
    PUBLISHER = {Dept. of Comp. Sci., University of Alberta},
ADDRESS = {Edmonton, Canada},
NOTE = {M Sc thesis, {\tt http://www.cs.ualberta.ca/\-\~{}piotr/Mizar/Doc/GL-thesis.ps}},
         YEAR = {2004}}

@BOOK{Hatcher,
      author     = {Hatcher, Allen},
      title      = {Algebraic Topology},
      publisher  = {Cambridge University Press},
      year       = {2002}}

@InCollection{BrouwerJordan,
  AUTHOR = {Gauld, David},
   TITLE = {Brouwer's {F}ixed {P}oint {T}heorem and
             the {J}ordan {C}urve {T}heorem},
     NOTE = {{\tt http://aitken.math.auckland.ac.nz/\~{}gauld/750-05/section5.pdf}}}

@BOOK{HardyWright,
    AUTHOR = {Hardy, G.H. and Wright, E.M.},
     TITLE = {An Introduction to the Theory of Numbers},
 PUBLISHER = {Oxford University Press},
      YEAR = 1980}

@BOOK{Minc78,
    AUTHOR = {Minc, H.},
     TITLE = {Permanents},
   JOURNAL = {Volume 6 of Encyclopedia of Mathematics and its applications},
 PUBLISHER = {Addison-Wesley},
      YEAR = 1978}

@BOOK{LeVeque,
       AUTHOR = {LeVeque, W. J.},
        TITLE = {Fundamentals of Number Theory},
    PUBLISHER = {Dover Publication},
         YEAR = {1996},
      ADDRESS = {New York}}

@BOOK{PFTB,
       AUTHOR = {Aigner, M. and Ziegler, G. M.},
        TITLE = {Proofs from {THE} {BOOK}},
    PUBLISHER = {Springer-Verlag},
         YEAR = {2004},
      ADDRESS = {Berlin Heidelberg New York}}

@BOOK{ModernComputerAlgebra,
   AUTHOR={von zur Gathen, J. and Gerhard, J.},
   TITLE={Modern {C}omputer {A}lgebra},
   PUBLISHER={Cambridge University Press},
   YEAR=1999}

@ARTICLE{SCHUR:1,
   AUTHOR={Schur, J.},
   TITLE={\"{U}ber algebraische {G}leichungen,
     die nur {W}urzeln mit negativen {R}ealteilen besitzen},
   JOURNAL={Zeitschrift f\"{u}r angewandte Mathematik und Mechanik},
   YEAR=1921,
   VOLUME=1,
   PAGES={307--311}}

@BOOK{Halmos74,
         AUTHOR = {Halmos, P.~R.},
          TITLE = {Measure Theory},
      PUBLISHER = {Springer-Verlag},
           YEAR = {1987}}

@BOOK{Clarke2000,
         AUTHOR = {Clarke, E. M. and Grumberg, O. and Peled, D.},
          TITLE = {Model Checking},
      PUBLISHER = {MIT Press},
           YEAR = {2000}}

@BOOK{SIERPINSKI:1,
    AUTHOR={Sierpi{\'n}ski, Wac{\l}aw},
    TITLE={Elementary Theory of Numbers},
    PUBLISHER={PWN, Warsaw},
    YEAR={1964}}

@Book{Golumbic,
 author     = {Golumbic, M. Ch.},
 title      = {Algorithmic Graph Theory and Perfect Graphs},
 publisher  = {Academic Press},
 address    = {New York},
 year       = {1980}}
 
@article{TY84,
  author    = {Tarjan, R. E. and Yannakakis, M.},
  title     = {Simple Linear-Time Algorithms to Test Chordality of Graphs,
               Test Acyclicity of Hypergraphs, and Selectively Reduce Acyclic
               Hypergraphs.},
  journal   = {SIAM J. Comput.},
  volume    = {13},
  number    = {3},
  year      = {1984},
  pages     = {566-579}}

@TECHREPORT{Geanakoplos:1996,
 AUTHOR={Geanakoplos, John},
 TITLE={Three Brief Proofs of {A}rrow's Impossibility Theorem},
 YEAR={1996},
 MONTH={April},
 INSTITUTION={Cowles Foundation, Yale University},
 TYPE={Cowles Foundation Discussion Papers},
 NOTE={Available at http://ideas.repec.org/p/cwl/cwldpp/1123r3.html},
 URL={http://ideas.repec.org/p/cwl/cwldpp/1123r3.html},
 NUMBER={1123R3}}

@BOOK{BCIAlgebras,
       AUTHOR = {Meng, Jie and Liu, YoungLin},
        TITLE = {An Introduction to {BCI}-algebras},
    PUBLISHER = {Shaanxi Scientific and Technological Press},
         YEAR = {2001}}

@BOOK{BCIAlgebras2,
       AUTHOR = {Huang, Yisheng},
        TITLE = {{BCI}-algebras},
    PUBLISHER = {Science Press},
         YEAR = {2006}}

@BOOK{Billingsley:1964,
 AUTHOR={Billingsley, P.},
 TITLE={Ergodic Theory and Information},
 PUBLISHER={John Wiley \& Sons},
 YEAR={1964}}

@BOOK{Hirasawa:1996,
 AUTHOR={Hirasawa, Shigeichi},
 TITLE={Information Theory},
 PUBLISHER={Baifukan CO.},
 YEAR={1996}}

@BOOK{HOPCROFT-ULLMAN:1979,
 AUTHOR={Hopcroft, John E. and Ullman, Jeffrey D.},
 TITLE={Introduction to Automata Theory, Languages and Computation},
 PUBLISHER={Addison-Wesley Publishing Company},
 YEAR={1979}}

@BOOK{WAITE-GOOS:1984,
 AUTHOR={ Waite, William M. and Goos, Gerhard},
 TITLE={Compiler Construction},
 PUBLISHER={Springer-Verlag New York Inc.},
 YEAR={1984}}

@BOOK{WALL-CHRISTIANSEN-ORWANT:2000,
 AUTHOR={Wall, Larry and Christiansen, Tom and Orwant, Jon},
 TITLE={Programming {P}erl, Third Edition},
 PUBLISHER={O'Reilly Media},
 YEAR={2000}}

@BOOK{BourbakiAlgI,
       AUTHOR = {Bourbaki, Nicolas},
        TITLE = {Elements of Mathematics. {A}lgebra {I}. {C}hapters 1-3},
    PUBLISHER = {Springer-Verlag},
         YEAR = {1989},
      ADDRESS = {Berlin, Heidelberg, New York, London, Paris, Tokyo}}

@BOOK{Apostol:1969,
 AUTHOR = {Apostol, Tom M.},
 TITLE = {Mathematical Analysis},
 PUBLISHER = {Addison-Wesley},
 YEAR = {1969}}

@BOOK{Furuya:57,
       AUTHOR = {Furuya, Shigeru},
        TITLE = {Matrix and Determinant},
    PUBLISHER = {Baifuukan (in Japanese)},
          YEAR = {1957}}

@BOOK{Gantmacher:59,
        AUTHOR = {Gantmacher, Felix R.},
         TITLE = {The Theory of Matrices},
     PUBLISHER = {AMS Chelsea Publishing},
          YEAR = {1959}}

@BOOK{lang-algebra,
  author = 	 {Lang, Serge},
  title = 	 {Algebra},
  publisher = 	 {Springer},
  year = 	 {2005},
  edition = 	 {3rd}}

@Book{kelley,
  author = {Kelley, John L.},
  title = {General Topology},
  publisher = {Springer-Verlag},
  year = {1955},
  volume = {27},
  series = {Graduate Texts in Mathematics}}

@BOOK{Chemnitius:1956,
 AUTHOR={Chemnitius, Fritz},
 TITLE={Differentiation und Integration ausgew\"ahlter Beispiele},
 PUBLISHER={VEB Verlag Technik, Berlin},
 YEAR={1956}}

@BOOK{HuaLooKeng:1957,
       AUTHOR = {Keng, Hua Loo},
        TITLE = {Introduction to Number Theory},
    PUBLISHER = {Beijing Science Publication},
         YEAR = {1957},
      ADDRESS = {China}}

@BOOK{Dexin:1965,
       AUTHOR = {Dexin, Zhang},
        TITLE = {Integer Theory},
    PUBLISHER = {Science Publication},
         YEAR = {1965},
      ADDRESS = {China}}

@BOOK{yoshida:1980,
 AUTHOR={Kosaku Yoshida},
 TITLE={Functional Analysis},
 PUBLISHER={Springer},
 YEAR={1980}}

@BOOK{miyadera:1972,
 AUTHOR={Isao Miyadera},
 TITLE={Functional Analysis},
 PUBLISHER={Riko-Gaku-Sya},
 YEAR={1972}}

@BOOK{Dunford:1958,
 AUTHOR={Dunford, N. J. and Schwartz, T.},
 TITLE={Linear operators {I}},
 PUBLISHER={Interscience Publ.},
 YEAR={1958}}

@article{euler1758a,
	author = {Euler, Leonhard},
	title = {Elementa Doctrinae Solidorum},
	journal = {Novi Commentarii Academiae Scientarum Petropolitanae},
	year = {1758},
	volume = {4},
	pages = {109-140}}

@book{proofs-and-refutations,
	author = {Lakatos, Imre},
	title = {Proofs and Refutations: The Logic of Mathematical Discovery},
	publisher = {Cambridge University Press},
	year = {1976},
	note = {Edited by John Worrall and Elie Zahar}}

@book{grunbaum2003,
	author = {Gr\"unbaum, Branko},
	title = {Convex Polytopes},
	publisher = {Springer},
	year = {2003},
	edition = {2nd},
	series = {Graduate Texts in Mathematics},
	number = {221}}

@book{brondsted1983,
	author = {Br{\o}ndsted, Arne},
	title = {An Introduction to Convex Polytopes},
	publisher = {Springer},
	year = {1983},
	series = {Graduate Texts in Mathematics}}

@article{poincare1893,
	author = {Poincar\'e, Henri},
	title = {Sur la G\'en\'eralisation d'un Th\'eor\`eme d'{E}uler relatif aux Poly\`edres},
	journal = {Comptes Rendus de S\'eances de l'Academie des Sciences},
	year = {1893},
	volume = {117},
	pages = {144}}

@article{poincare1899,
	author = {Poincar\'e, Henri},
	title = {Compl\'ement \`a l'Analysis Situs},
	journal = {Rendiconti del Circolo Matematico di Palermo},
	year = {1899},
	volume = {13},
	pages = {285-343}}

@book{Schwartz:1981,
       author = {Schwartz, Laurent},
       title = {Cours d'analyse},
       publisher = {Hermann},
       year = {1981}}
       
@article{berline97kappadenotational,
    author = {Berline, Chantal and Grue, Klaus},
    title = {A kappa-Denotational Semantics for Map Theory in {ZFC} + {SI}},
    journal = {Theoretical Computer Science},
    volume = {179},
    number = {1-2},
    pages = {137-202},
    year = {1997},
    url = {citeseer.ist.psu.edu/berline97kappadenotational.html}}


@book{krivine93,
  author =      {Krivine, J.L.},
  title =       {Lambda-calculus, types and models},
  isbn = {0-13-062407-1},
  publisher =   {Ellis \& Horwood},
  year =        {1993}}

@BOOK{Chen:1978,
 AUTHOR={Chen, Chuanzhang},
 TITLE={Mathematical Analysis},
 PUBLISHER={Higher Education Press, Beijing},
 YEAR={1978}}

@BOOK{ThomasJech2002,
       AUTHOR = {Jech, T. J.},
        TITLE = {Set Theory},
    PUBLISHER = {Springer-Verlag},
         YEAR = {2002},
      ADDRESS = {Berlin Heidelberg New York}}

@BOOK{Beran:1984,
      AUTHOR = {Beran, Ladislav},
       TITLE = {Orthomodular Lattices. {A}lgebraic Approach},
   PUBLISHER = {Academiai Kiado},
        YEAR = {1984}}

@BOOK{Halmos:1956,
       AUTHOR = {Halmos, Paul R.},
        TITLE = {Lectures on Ergodic Theory},
    PUBLISHER = {The Mathematical Society of Japan},
         YEAR = {1956},
         NOTE = {No.3}}

@BOOK{Renhong:1999,
 AUTHOR={Wang, Renhong},
 TITLE={Numerical approximation},
 PUBLISHER={Higher Education Press, Beijing},
 YEAR={1999}}

@BOOK{Kawamoto-Nakamura:1996,
 AUTHOR={Kawamoto, Pauline N. and Nakamura, Yatsuka},
 TITLE={On Cell {P}etri Nets},
 PUBLISHER={Journal of Applied Functional Analysis},
 YEAR={1996}}

@BOOK{GolubWilkinson,
 AUTHOR = {Gene H. Golub and J. H. Wilkinson},
 TITLE = {Ill-conditioned eigensystems and the computation of the
            {J}ordan normal form},
 PUBLISHER = {SIAM Review, vol. 18, nr. 4, pp. 578--619},
 YEAR={1976}}

@Book{Welsh:1976,
  author =	 {Welsh, D. J. A.},
  title = 	 {Matroid theory},
  publisher = 	 {Academic Press},
  year = 	 {1976},
  address =	 {London, New York, San Francisco}}

@InBook{Lipski,
  author =	 {Lipski, Witold},
  title = 	 {Kombinatoryka dla programist\'ow},
  chapter = 	 {Matroidy},
  publisher = 	 {Wydawnictwo Naukowo-Techniczne},
  year = 	 {1982},
  pages =	 {163--169}}

@InCollection{Freek-100-theorems,
  AUTHOR = {Wiedijk, Freek},
   TITLE = {Formalizing 100 Theorems},
     NOTE = {{\tt http://www.cs.ru.nl/\~{}freek/100/}}}

@article{Vuillemin1983,
 author={Vuillemin, E. Jean},
 journal={The VLSI Journal},
 pages={39--52},
 title={A Very Fast Multiplication Algorithm for {VLSI} Implementation, Integration},
 volume={1},
 number={1},
 year={1983}}

@BOOK{HerstenWinter,
        AUTHOR = {Herstein, I.N. and Winter, David J.},
         TITLE = {Matrix Theory and Linear Algebra},
     PUBLISHER = {Macmillan},
          YEAR = {1988}}

@BOOK{Korn,
       AUTHOR = {Korn, G.A. and Korn, T.M.},
        TITLE = {Mathematical Handbook for Scientists and Engineers},
    PUBLISHER = {Dover Publication},
         YEAR = {2000},
      ADDRESS = {New York}}

@ARTICLE{CINTA,
      AUTHOR  = {Victor Shoup},
      TITLE   = {A Computational Introduction to Number Theory and Algebra},
      JOURNAL = {Cambridge University Press},
      YEAR    = {2008}}

@BOOK{Murray:1974,
 AUTHOR={Murray R. Spiegel},
 TITLE={Theory and Problems of Vector Analysis},
 PUBLISHER={McGraw-Hill},
 YEAR={1974}}

@ARTICLE{Mousavi:2001,
 AUTHOR={Mousavi, Amin and Jabedar-Maralani, Parviz},
 TITLE={Relative Sets and Rough Sets},
 JOURNAL={Int. J. Appl. Math. Comput. Sci.},
 VOLUME = {11},
 NUMBER = {3},
 PAGES = {637--653},
 YEAR={2001}}

@ARTICLE{Yao:1993,
 AUTHOR={Yao, Y.Y.},
 TITLE={Interval-set Algebra for Qualitative Knowledge Representation},
 JOURNAL={Proc. 5-th Int. Conf. Computing and Information},
 PUBLISHER = {IEEE Computer Society Press},
 PAGES = {370--375},
 YEAR={1993}}

@BOOK{ENGEL:BM51,
 AUTHOR={Engelking, Ryszard},
 TITLE={Teoria wymiaru},
 PUBLISHER={PWN},
 YEAR={1981}}

@article{Dilworth50,
 author     = {R. P. Dilworth},
 title      = {A {D}ecomposition {T}heorem for {P}artially {O}rdered {S}ets},
 journal    = {Annals of Mathematics},
 volume     = {51},
 number     = {1},
 year      = {1950},
 pages     = {161-166}}

@article{Perles63,
  author    = {M. A. Perles},
  title     = {A {P}roof of {D}ilworth's {D}ecomposition {T}heorem for
               {P}artially {O}rdered {S}ets},
  journal   = {Israel Journal of Mathematics},
  volume    = {1},
  year      = {1963},
  pages     = {105-107}}

@article{Mirsky71,
  author    = {L. Mirsky},
  title     = {A {D}ual of {D}ilworth's {D}ecomposition {T}heorem},
  journal   = {The American Mathematical Monthly},
  volume    = {78},
  number    = {8},
  year      = {1971},
  pages     = {876-877}}

@article{ES35,
  author    = {P. Erd\H{o}s and G. Szekeres},
  title     = {A combinatorial problem in geometry},
  journal   = {Compositio Mathematica},
  volume    = {2},
  year      = {1935},
  pages     = {463-470}}

@BOOK{DUDA:BM61,
AUTHOR={Duda, Roman},
TITLE={Wprowadzenie do topologii},
PUBLISHER={PWN},
YEAR={1986}}

@article{Pawlak1982,
  author    = {Z. Pawlak},
  title     = {Rough sets},
  journal   = {International Journal of Parallel Programming},
  volume    = {11},
  year      = {1982, doi:10.1007/BF01001956},
  pages     = {341-356}}

@BOOK{Spiegel:1959,
 AUTHOR={Murray R. Spiegel},
 TITLE={Vector Analysis and an Introduction to Tensor Analysis},
 PUBLISHER={McGraw-Hill Book Company, New York},
 YEAR={1959}}

@BOOK{Rudin:1976,
 AUTHOR={Rudin, Walter},
 TITLE={Principles of Mathematical Analysis},
 PUBLISHER={MacGraw-Hill},
 YEAR={1976}}

@BOOK{Winskel:1993,
 AUTHOR={Glynn Winskel},
 TITLE={The Formal Semantics of Programming Languages},
 PUBLISHER={The MIT Press},
 YEAR={1993}}

@BOOK{Keith:1984,
 AUTHOR={Keith E. Hirst},
 TITLE={Numbers, Sequences and Series},
 PUBLISHER={Butterworth-Heinemann},
 YEAR={1984}}

@ARTICLE{Veblen,
 AUTHOR={Veblen, Oswald},
TITLE={Continuous Increasing Functions of Finite and Transfinite Ordinals},
JOURNAL={Transactions of the American Mathematical Society},
VOLUME=9,
NUMBER=3,
PAGES={280–292},
YEAR= {1908, doi:10.2307/1988605}}

@article{Mycielski55,
 author     = {J. Mycielski},
 title      = {Sur le coloriage des graphes},
 journal    = {Colloquium Mathematicum},
 volume     = {3},
 year       = {1955},
 pages      = {161-162}}

@article{LUP95,
  author    = {M. Larsen and J. Propp and D. Ullman},
  title     = {The fractional chromatic number of {M}ycielski's graphs},
  journal   = {Journal of Graph Theory},
  volume    = {19},
  year      = {1995},
  pages     = {411-416}}

@BOOK{JLee2000,
       AUTHOR = {John M. Lee},
        TITLE = {Introduction to Topological Manifolds},
    PUBLISHER = {Springer-Verlag},
         YEAR = {2000},
      ADDRESS = {New York Berlin Heidelberg}}

@ARTICLE{Schwartz:1967,
      AUTHOR  = {Laurent Schwartz},
      TITLE   = {Cours d'Analyse, Vol. 1},
      JOURNAL = {Hermann Paris},
      YEAR    = 1967}

@ARTICLE{BOURBAKI:1-5,
      AUTHOR  = {Nicolas Bourbaki},
      TITLE   = {Topological Vector Spaces: Chapters 1-5},
      JOURNAL = {Springer},
      YEAR    = 1981}

@ARTICLE{Micci:2002,
      AUTHOR  = {Daniele Micciancio and Shafi Goldwasser},
      TITLE   = {Complexity of Lattice Problems:
      A Cryptographic Perspective (The International Series
      in Engineering and Computer Science)},
      PUBLISHER={Springer},
      YEAR    = 2002}

@ARTICLE(CA,
      AUTHOR  = {Laurent Schwartz},
      TITLE   = {Cours d'analyse, Vol. 1},
      JOURNAL = {Hermann Paris},
      YEAR    = 1967)

@book{Conway:2001,
    AUTHOR = {Conway, J. H.},
     TITLE = {On numbers and games},
   EDITION = {Second},
 PUBLISHER = {A K Peters Ltd.},
   ADDRESS = {Natick, MA},
      YEAR = {2001},
     PAGES = {xii+242},
      ISBN = {1-56881-127-6}}

@Book{Salwicki,
  author = 	 {Gra\.zyna Mirkowska and Andrzej Salwicki},
  title = 	 {Algorithmic Logic},
  publisher = 	 {PWN-Polish Scientific Publisher},
  year = 	 1987}

@BOOK{KroMer,
 AUTHOR={Kr\"oger, Fred and Merz, Stephan},
 TITLE={Temporal Logic and State Systems},
 PUBLISHER={Springer-Verlag},
 YEAR={2008}}

@book{georgii:2004,
author={Georgii, Hans-Otto},
title={Stochastik, Einf\"uhrung
  in die Wahrscheinlichkeitstheorie und Statistik},
edition={2},
publisher={deGruyter},
year={2004},
ADDRESS={Berlin}}

@book{klenke:2006,
author={Klenke, Achim},
title={Wahrscheinlichkeitstheorie},
publisher={Springer-Verlag},
year={2006},
ADDRESS={Berlin, Heidelberg}}

@ARTICLE{MazurUlam,
 AUTHOR={Mazur, Stanis{\l}aw and Ulam, Stanis{\l}aw},
 TITLE={Sur les transformationes isom\'etriques d'espaces vectoriels norm\'es},
 JOURNAL={C. R. Acad. Sci. Paris},
 NUMBER={194},
 PAGES={946--948},
 YEAR={1932}}

@MISC{Jussi,
 AUTHOR={V\"{a}is\"{a}l\"{a}, Jussi},
 TITLE={A proof of the Mazur-Ulam theorem},
 URL={http://www.helsinki.fi/~jvaisala/mazurulam.pdf}}

@BOOK{BSS99,
      AUTHOR = {I. Blake, G. Seroussi and N. Smart},
      TITLE = {Elliptic Curves in Cryptography},
      PUBLISHER = {Cambridge University Press},
      SERIES = {London Mathematical Society Lecture Note Series},
      NUMBER = {265},
      YEAR = {1999}}

@BOOK{SIEKLUCKI:BM53,
 AUTHOR={Sieklucki, Karol},
 TITLE={Geometria i topologia},
 PUBLISHER={PWN},
 YEAR=1979}

@BOOK{lothaire2002algebraic,
  AUTHOR={Lothaire, M.},
  TITLE={Algebraic combinatorics on words},
  PUBLISHER={Cambridge Univ Pr},
  YEAR={2002}}

@article{pohlers1992introduction,
  title={An introduction to mathematical logic},
  author={Pohlers, W. and Gla{\ss}, T.},
  journal={Vorlesungsskriptum, WS},
  volume={93},
  year={1992}}

@book{ebbinghaus1994mathematical,
  title={Mathematical logic},
  author={Ebbinghaus, H.D. and Flum, J. and Thomas, W.},
  year={1994},
  publisher={Springer}}

@article{caminati2009yet,
  title={{Yet another proof of Goedel's completeness theorem for first-order classical logic}},
  author={Caminati, M.B.},
  journal={Arxiv preprint arXiv:0910.2059},
  year={2009}}

@ARTICLE{Cayley:1854,
 AUTHOR={Cayley, Arthur},
 TITLE={On the theory of groups as depending on the symbolic equation $\Theta^n=1$},
 JOURNAL={Phil. Mag.},
 VOLUME={7},
 NUMBER={4},
 PAGES={40--47},
 YEAR=1854}