@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} {M}izar 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}}

@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}}

@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},
 publisher = {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}}

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

@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, T.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},
 publisher = {DIMACS},
          URL = {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}}

@ARTICLE{MatTry77,
       AUTHOR = {Matuszewski, Roman and Trybulec, Andrzej},
        TITLE = {Certain algorithm of classification in metric spaces},
    PUBLISHER = {Warsaw University, Bialystok Campus},
         YEAR = {1977},
       VOLUME = {V},
        PAGES = {117--123},
      NUMBER  = {20},
       JOURNAL = {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},
          PAGES = {69--85}}

@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},
          URL = {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},
    URL = {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},
     URL = {https://www.math.auckland.ac.nz/class750/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 = {1974}}

@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},
 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={Yoshida, Kosaku},
 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 = {http://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},
     URL = {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    = {Pawlak, Zdzis{\l}aw},
  title     = {Rough sets},
  journal   = {International Journal of Parallel Programming},
  volume    = {11},
  year      = {1982},
doi = {10.1007/BF01001956},
  pages     = {341--356}}

@BOOK{Spiegel:1959,
 AUTHOR={Spiegel, Murray R.},
 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={Winskel, Glynn},
 TITLE={The Formal Semantics of Programming Languages},
 PUBLISHER={The MIT Press},
 YEAR={1993}}

@BOOK{Keith:1984,
 AUTHOR={Hirst, Keith E.},
 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     = {Mycielski, J.},
 title      = {Sur le coloriage des graphes},
 journal    = {Colloquium Mathematicum},
 volume     = {3},
 year       = {1955},
 pages      = {161--162}}

@article{LUP95,
  author    = {Larsen, M. and Propp, J. and Ullman, D.},
  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 = {Lee, John M.},
        TITLE = {Introduction to Topological Manifolds},
    PUBLISHER = {Springer-Verlag},
         YEAR = {2000},
      ADDRESS = {New York Berlin Heidelberg}}

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

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

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

@ARTICLE{CA,
      AUTHOR  = {Schwartz, Laurent},
      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 = 	 {Mirkowska, Gra\.zyna and Salwicki, Andrzej},
  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={2nd},
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}}

@ARTICLE{Jussi,
 AUTHOR={V\"{a}is\"{a}l\"{a}, Jussi},
 TITLE={A proof of the {M}azur-{U}lam theorem},
   URL={http://www.helsinki.fi/\textasciitilde jvaisa\-la/mazur\-ulam.pdf}}

@BOOK{BSS99,
      AUTHOR = {Blake, I. and Seroussi, G. and Smart, N.},
      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}}

@ARTICLE{caminati2010basic,
  author = {Caminati, M.B.},
  title = {{Basic first-order model theory in {M}izar}},
  journal = {Journal of Formalized Reasoning},
  year = {2010},
  volume = {3},
  pages = {49--77},
  number = {1},
  issn = {1972-5787}}

@book{follmerschied:2004,
  author={F\"ollmer, Hans and Schied, Alexander},
  title={Stochastic Finance: An Introduction in Discrete Time},
  edition={2nd},
  volume={27},
  series={Studies in Mathematics},
  publisher={de Gruyter},
  year={2004},
  ADDRESS={Berlin}}

@BOOK{EmilArtin,
  AUTHOR = {Artin, Emil},
  TITLE = {Algebraic Numbers and Algebraic Functions},
  publisher = {Gordon and Breach Science Publishers},
  year = {1994}}

@BOOK{Heijmans:1994,
 AUTHOR={Heijimans, H.J.A.M.},
 TITLE={Morphological Image Operators},
 PUBLISHER={Academic Press},
 YEAR={1994}}

@BOOK{Soille:2003,
 AUTHOR={Soille, P.},
 TITLE={Morphological Image Analysis: Principles and Applications},
 PUBLISHER={Springer},
 YEAR={2003}}

@ARTICLE{FIPS,
      AUTHOR  = {U.S. Department of Commerce/National Institute of Standards and Technology},
      TITLE   = {FIPS PUB 46-3, DATA ENCRYPTION STANDARD ({D}{E}{S})},
      URL     = {http://csrc.nist.gov/publications/\-fips/\-fips46-3/fips46-3.pdf},
      JOURNAL = {Federal Information Processing Standars Publication},
      YEAR    = 1999}

@Article{Bancerek2006,
  author = 	 {Bancerek, Grzegorz},
  title = 	 {Information Retrieval and Rendering with {M}{M}{L} Query},
  journal = 	 {Lecture Notes in Computer Science},
  year = 	 2006,
  volume =	 4108,
  pages =	 {266--279}}

@book{Harary69,
  Author = {Harary, Frank},
  Title = {Graph theory},
  Publisher = {Addison-Wesley},
  Year = {1969}}

@book{Veblen31,
  Author = {Veblen, Oswald},
  Title = {Analysis Situs},
  Publisher = {AMS Colloquium Publications},
  Volume={V},
  Year = {1931}}

@BOOK{Knuth2,
      AUTHOR = {Knuth, Donald E.},
      TITLE = {Art of Computer Programming},
      PUBLISHER = {Volume 2: Seminumerical Algorithms, 3rd Edition, Addison-Wesley Professional},
      YEAR = {1997}}

@ARTICLE{NZMATH,
      AUTHOR  = {NZMATH development Group},
      TITLE   = {NZMATH},
        URL   = {http://tnt.math.se.tmu.ac.jp/nzmath/}}

@BOOK{HH90,
      AUTHOR = {Heuser, H.},
      TITLE = {Lehrbuch der Analysis},
      PUBLISHER = {B.G. Teubner Stuttgart},
      YEAR = {1990}}


@BOOK{Ebbinghaus2007,
 AUTHOR={Ebbinghaus, H.-D. and Flum, J. and Thomas, W.},
 TITLE = {Einf\"uhrung in die Mathematische Logik},
 YEAR = {2007},
 PUBLISHER = {Springer-Verlag, Berlin Heidelberg}}

@BOOK{Goedel:1930,
 AUTHOR={G\"odel, Kurt},
 TITLE={Die Vollst\"andigkeit der Axiome des logischen Funktionenkalk\"uls},
 PUBLISHER={Monatshefte f\"ur Mathematik und Physik 37},
 YEAR={1930}}

@ARTICLE{MAlbert,
  AUTHOR =       {Michael, Albert},
  TITLE =        {Notes On The Friendship Theorem},
    URL =        {http://www.math.auckland.ac.nz/\-\~{}olympiad/\-Training/\-2006/\-friendship.pdf}}


@InBook{KlopTRS,
  editor = 	 {Abramsky, S. and Gabbay, D.M. and Maibaum, T.S.E.},
  title = 	 {Handbook of Logic in Computer Science},
  chapter = 	 {Term Rewriting Systems},
  publisher = 	 {Oxford University Press},
  year = 	 {1992},
  address = 	 {New York},
  pages = 	 {1--116},
  url   = 	 {http://www.informatik.\-uni-bremen.\-de/\-agbkb/\-lehre/\-rbs/texte/Klop-TR.pdf}}


@BOOK{HardyWright2007,
       AUTHOR = {Hardy, G.H. and Wright, E.M.},
        TITLE = {An Introduction to the Theory of Numbers},
    PUBLISHER = {Posts and Telecom Press},
         YEAR = {2007},
      ADDRESS = {China}}

@BOOK{Schwartz:1967:2:5,
 AUTHOR={Schwartz, Laurent},
 TITLE={Cours d'analyse II, Ch. 5},
 PUBLISHER={HERMANN, Paris},
 YEAR=1967}

@BOOK{Kosaku:1996,
 AUTHOR={Yosida, Kosaku},
 TITLE={Functional Analysis},
 PUBLISHER={Springer Classics in Mathematics},
 YEAR=1996}

@BOOK{Unb93,
      AUTHOR = {Unbehauen, Rolf},
      TITLE = {Netzwerk- und Filtersynthese: Grundlagen und Anwendungen},
      EDITION = {Fourth},
      PUBLISHER = {Oldenbourg-Verlag},
      YEAR = {1993}}

@ARTICLE{Zhu:2007,
 AUTHOR = {Zhu, William},
 TITLE = {Generalized Rough Sets Based on Relations},
 JOURNAL = {Information Sciences},
 VOLUME = 177,
 PAGES = {4997--5011},
 YEAR=2007}

@article{SkowronS96,
  author    = {Skowron, Andrzej and Stepaniuk, Jaros{\l}aw},
  title     = {Tolerance Approximation Spaces},
  journal   = {Fundamenta Informaticae},
  volume    = {27},
  number    = {2/3},
  year      = {1996}, 
doi = {10.3233/FI-1996-272311},
  pages     = {245--253}}

@inproceedings{GrabowskiJ10,
  author    = {Grabowski, Adam and
               Jastrz\k{e}bska, Magdalena},
  title     = {A Note on a Formal Approach to Rough Operators},
  booktitle     = {Rough Sets and Current Trends in Computing -- 7th International
               Conference, RSCTC 2010, Warsaw, Poland, June 28-30, 2010.
               Proceedings},
  pages     = {307--316},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6086},
  year      = {2010}, 
doi = {10.1007/978-3-642-13529-3\_33},
  EDITOR = {Marcin S. Szczuka and Marzena Kryszkiewicz et al.}}

@article{Yao96,
  author    = {Yao, Y.Y.},
  title     = {Two Views of the Theory of Rough Sets in Finite Universes},
  journal   = {International Journal of Approximate Reasoning},
  volume    = {15},
  number    = {4},
  year      = {1996},
doi = {10.1016/S0888-613X(96)00071-0},
  pages     = {291--317}}

@BOOK{ECC:2006,
  AUTHOR = {Moreira, J.C. and Farrell, P.G.},
  TITLE = {Essentials of Error-Control Coding},
  PUBLISHER = {John Wiley \& Sons Ltd, The Atrium, Southern Gate, Chichester},
  YEAR = {2006}}

@ARTICLE{Lai1994,
  AUTHOR = {Lai, X.},
  TITLE = {Higher Order Derivatives and Differential Cryptoanalysis},
  JOURNAL = {Communications and Cryptography},
  PAGES = {227--233},
  PUBLISHER = {Kluwer Academic Publishers},
  YEAR = {1994}}
  
  @BOOK{Engelking:1968,
   AUTHOR = {Engelking, Ryszard},
   TITLE = {Outline of General Topology},
   PUBLISHER = {North-Holland Publishing Company},
   YEAR = {1968}}
  
  @BOOK{SteenSeebach:1978,
   AUTHOR={Steen, Lynn Arthur and Seebach, J. Arthur Jr.},
   TITLE={Counterexamples in Topology},
   PUBLISHER={Springer-Verlag},
   YEAR={1978}}
   
   @article{Briggs2000,
     title={Simple Divisibility Rules for the 1st 1000 Prime Numbers},
     author={Briggs, C.C.},
     journal={arXiv preprint arXiv:math/0001012},
     year={2000},
      url={http://arxiv.org/abs/math/0001012v1}}
  
  @BOOK{Gauss:1986,
   AUTHOR = {Gauss, Carl Friedrich},
   TITLE = {Disquisitiones Arithmeticae},
   PUBLISHER = {Springer},
   YEAR = {1986},
   ADDRESS = {New York},
   NOTE = {English translation}}
  
  @ARTICLE{Guy:1994,
   AUTHOR = {Guy, Richard K.},
   TITLE = {Every number is expressible as a sum of how many polygonal numbers?},
   JOURNAL = {American Mathematical Monthly},
   YEAR = {1994},
   VOLUME = {101},
   PAGES={169--172}}
  
  @BOOK{Weil:1983,
   AUTHOR = {Weil, Andr\'e},
   TITLE = {Number Theory. {A}n Approach through History from {H}ammurapi to {L}egendre},
   PUBLISHER = {Birkh\"auser},
   YEAR = {1983},
   ADDRESS = {Boston, Mass.}}
  
  @BOOK{Heath:1921,
   AUTHOR = {Heath, Thomas L.},
   TITLE = {A History of {G}reek Mathematics: From {T}hales to {E}uclid, Vol. {I}},
   PUBLISHER = {Courier Dover Publications},
 YEAR = {1921}}
 
@BOOK{Weil:1979,
      AUTHOR = {Weil, Andr\'e},
      TITLE = {Number Theory for Beginners},
      PUBLISHER = {Springer-Verlag},
      YEAR = {1979}}
      
 @BOOK{HUFFMAN:1952,
      AUTHOR = {Huffman, D. A.},
      TITLE = {A method for the construction of minimum-redundancy codes},
      PUBLISHER = {Proceedings of the I.R.E},
      YEAR = {1952}}     
      
@ARTICLE{Kuzyka,
 AUTHOR = {Wojszko, Krzysztof and Kuzyka, Artur},
 TITLE= {Formalization of Commodity Space and Preference Relation in {M}izar},
 JOURNAL = {Mechanized Mathematics and Its Applications},
 YEAR = {2005},
 VOLUME = {4},
 PAGES = {67--74}}

@ARTICLE{Aumann,
 AUTHOR = {Aumann, Robert J.},
 TITLE = {Utility Theory Without the Completeness Axiom},
 JOURNAL = {Econometrica},
 YEAR = {1962},
 VOLUME = {30},
 NUMBER = {3},
 PAGES = {445--462}}

@ARTICLE{Schumm,
 AUTHOR = {Schumm, George F.},
 TITLE = {Transitivity, Preference, and Indifference},
 JOURNAL = {Philosophical Studies},
 YEAR = {1987},
 VOLUME = {52},
 PAGES = {435--437}}

@BOOK{Arrow,
 AUTHOR = {Arrow, Kenneth J.},
 TITLE = {Social Choice and Individual Values},
 YEAR = {1963},
 PUBLISHER = {Yale University Press}}

@BOOK{Hallden,
 AUTHOR = {Halld\'en, S\"oren},
 TITLE = {On the Logic of Better},
 YEAR = {1957},
 PUBLISHER = {Lund: Library of Theoria}}

@BOOK{Panek,
 AUTHOR = {Panek, Emil},
 TITLE = {Podstawy ekonomii matematycznej},
 PUBLISHER = {Uniwersytet Ekonomiczny w Poznaniu},
 YEAR = {2005},
 NOTE = {In Polish}}

@ARTICLE{FIPS:197,
  AUTHOR = {U.S. Department of Commerce/National Institute of
    Standards and Technology},
  TITLE = {{F}{I}{P}{S} {P}{U}{B} 197, {A}dvanced {E}ncryption {S}tandard ({A}{E}{S})},
  JOURNAL = {Federal Information Processing Standars Publication},
  YEAR = {2001},
  URL = {http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf}}

@BOOK{Borceaux,
       AUTHOR = {Borceaux, Francis},
        TITLE = {Handbook of Categorical Algebra I. {B}asic Category Theory},
    PUBLISHER = {Cambridge University Press},
         YEAR = {1994},
       VOLUME = {50},
       SERIES = {Encyclopedia of Mathematics and its Applications},
      ADDRESS = {Cambridge}}

@BOOK{Adamek:2009,
       AUTHOR = {Adamek, Jiri and Herrlich, Horst and Strecker, George E.},
        TITLE = {Abstract and Concrete Categories: The Joy of Cats},
    PUBLISHER = {Dover Publication},
         YEAR = {2009},
      ADDRESS = {New York}}

@ARTICLE{Nachbin,
 AUTHOR={Nachbin, Leopoldo},
 TITLE={Une propri\'et\'e characteristique des algebres booleiennes},
 JOURNAL={Portugaliae Mathematica},
 YEAR=1947,
 VOLUME=6,
 PAGES={115--118}}

@ARTICLE{StoneRepr,
 AUTHOR={Stone, Marshall H.},
 TITLE={The Theory of Representations of {B}oolean Algebras},
 JOURNAL={Transactions of the American Mathematical Society},
 YEAR=1936,
 VOLUME=40,
 PAGES={37--111}}

@BOOK{Gratzer2011,
 AUTHOR={Gr\"atzer, George},
 TITLE={Lattice Theory: Foundation},
 YEAR=2011,
 PUBLISHER = {Birkh\"auser}}

@BOOK{Balbes,
 AUTHOR={Balbes, Raymond and Dwinger, Philip},
 TITLE={Distributive Lattices},
 YEAR=1975,
 PUBLISHER = {University of Missouri Press}}

@BOOK{Wang:1998,
 AUTHOR={Wang, Jiacun},
 TITLE={Timed Petri Nets, Theory and Application},
 PUBLISHER={Kluwer Academic Publishers},
 YEAR=1998}

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

@BOOK{Engelking:1989,
       AUTHOR = {Engelking, Ryszard},
        TITLE = {General Topology},
    PUBLISHER = {Heldermann Verlag},
         YEAR = {1989},
      ADDRESS = {Berlin}}

@BOOK{Engelking:1978,
       AUTHOR = {Engelking, Ryszard},
        TITLE = {Dimension Theory},
    PUBLISHER = {North-Holland},
         YEAR = {1978},
      ADDRESS = {Amsterdam}}

@BOOK{Davey:2002,
  AUTHOR = {Davey, B.A. and Priestley, H.A.},
  TITLE = {Introduction to Lattices and Order},
  PUBLISHER = {Cambridge University Press},
  YEAR = 2002}

@BOOKLET{Schmets:2004,
TITLE = {Th{\'e}orie de la mesure},
AUTHOR = {Schmets, Jean},
HOWPUBLISHED = {Notes de cours, Universit\'e de Li\`ege, 146 pages},
YEAR = {2004},
LANGUAGE={French},
PAGES={1--4},
url = {http://www.anmath.ulg.ac.be/js/ens/tm.pdf}}

@ARTICLE{GOGUADZE:2003,
year={2003},
issn={0001-4346},
journal={Mathematical Notes},
volume={74},
issue={3-4},
doi={10.1023/A:1026102701631},
title={About the Notion of Semiring of Sets},
publisher={Kluwer Academic Publishers-Plenum Publishers},
author={Goguadze, D.F.},
pages={346--351}}

@ARTICLE{2011arXiv1103.6166P,
   author = {Patriota, A.~G},
    title = {A note on {C}arath\'{e}odory's Extension Theorem},
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1103.6166},
     year = 2011,
   url = {http://adsabs.harvard.edu/abs/2011arXiv1103.6166P}}

@ARTICLE{Buchmann:1992,
      AUTHOR  = {Buchmann, J. and M\"{u}ller, V.},
      TITLE   = {Primality Testing},
      URL={http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.1952},
      YEAR    = 1992}

@BOOK{Baker:1984,
 AUTHOR={Baker, Alan},
 TITLE={A Concise Introduction to the Theory of Numbers},
 PUBLISHER={Cambridge University Press},
 YEAR=1984}

@ARTICLE{GrabowskiFI:2013,
AUTHOR = {Grabowski, Adam},
TITLE = {Automated Discovery of Properties of Rough Sets},
JOURNAL = {Fundamenta Informaticae},
VOLUME = {128},
YEAR = {2013},
PAGES = {65--79},
DOI = {10.3233/FI-2013-933}}

@ARTICLE{BALLOT,
  AUTHOR =       {Renault, M.},
  TITLE =        {Four Proofs of the Ballot Theorem},
  JOURNAL =      {Mathematics Magazine},
  YEAR =         {2007},
  volume =       {80},
  number =       {5},
  pages =        {345--352},
  month =        {December}}

@article{Cauchy-AFP,
  author  = {Porter, Benjamin},
  title   = {Cauchy's Mean Theorem and the {C}auchy-{S}chwarz Inequality},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2006,
  note    = {\url{http://afp.sf.net/entries/Cauchy.shtml}, Formal proof development},
  ISSN    = {2150-914x}}

@BOOK{Schwabhauser:1983,
 AUTHOR = {Schwabh\"auser, Wolfram and Szmielew, Wanda and Tarski, Alfred},
 TITLE = {Metamathematische Methoden in der Geometrie},
 YEAR = {1983},
 PUBLISHER = {Springer-Verlag, Berlin, Heidelberg, New York, Tokyo}}

@INPROCEEDINGS{Narboux:2007,
       AUTHOR = {Narboux, Julien},
        TITLE = {Mechanical theorem proving in {T}arski's geometry},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
      BOOKTITLE = {Automated Deduction in Geometry},
      EDITOR = {F. Botana and T. Recio},
         YEAR = {2007},
       VOLUME = {4869},
        PAGES = {139--156}}

@ARTICLE{TarskiGivant,
 AUTHOR = {Tarski, Alfred and Givant, Steven},
 TITLE = {Tarski's system of geometry},
 JOURNAL = {Bulletin of Symbolic Logic},
 YEAR = 1999,
 VOLUME = 5,
 NUMBER = 2,
 PAGES={175--214}}

@BOOK{Chartrand:1985,
 AUTHOR={Chartrand, Gary},
 TITLE={Introductory Graph Theory},
 PUBLISHER={New York: Dover},
 YEAR=1985}

@BOOK{Wada:1981,
 AUTHOR={Wada, Hideo},
 TITLE={The World of Numbers (in {J}apanese)},
 PUBLISHER={Iwanami Shoten},
 YEAR=1984}

@book{analysis1:2001,
  author={Forster, Otto},
  title={Analysis 1},
  edition={6th},
  publisher={Vieweg-Verlag},
  year={2001},
  ADDRESS={Braunschweig/Wiesbaden}}

@book{Mendelson,
  author = {Mendelson, Elliott},
  title = {Introduction to Mathematical Logic},
  publisher = {Chapman & Hall/CRC},
  note = {\url{http://books.google.pl/books?id=ZO1p4QGspoYC}},
  year = {1997}}

@article{SwamyRao1981,
  author    = {Swamy, U.M. and Rao, G.C.},
  title     = {Almost Distributive Lattices},
  journal   = {Journal of Australian Mathematical Society},
  volume    = {31},
  year      = {1981},
  pages     = {77--91}}

@article{GADL:2009,
  author    = {Rao, G.C. and Bandaru, R.K. and Rafi, N.},
  title     = {Generalized Almost Distributive Lattices -- {I}},
  journal   = {Southeast Asian Bulletin of Mathematics},
  volume    = {33},
  year      = {2009},
  pages     = {1175--1188}}

@BOOK{Coxeter:1967,
 AUTHOR={Coxeter, H.S.M. and Greitzer, S.L.},
 TITLE={Geometry Revisited},
 PUBLISHER={The Mathematical Association of America (Inc.)},
 YEAR=1967}

@book{Hatton1731,
  Title                    = {An intire system of {A}rithmetic: or, {A}rithmetic in all its parts},
  Author                   = {Hatton, E.},
  Publisher                = {Printed for G. Strahan},
  Year                     = {1731},
  Number                   = {6},
  Timestamp                = {2014.12.08},
  note = {\url{http://books.google.pl/books?id=urZJAAAAMAAJ}}}

@Article{Mostafa2005,
  Title                    = {A New Approach to Polynomial Identities},
  Author                   = {Mostafa, M.I.},
  Journal                  = {The Ramanujan Journal},
  Year                     = {2005},
  Number                   = {4},
  Pages                    = {423--457},
  Volume                   = {8},
  Doi                      = {10.1007/s11139-005-0272-3},
  ISSN                     = {1382-4090},
  Keywords                 = {polynomial identities; formal derivation; sums of like powers;
Fibonacci numbers; Lucas numbers; recurrence sequences},
  Language                 = {English},
  Publisher                = {Kluwer Academic Publishers},
  Timestamp                = {2014.12.08},
  Url                      = {http://dx.doi.org/10.1007/s11139-005-0272-3}}

@Article{Nowak1998,
  Title                    = {On Differences of Two k-th Powers of Integers},
  Author                   = {Nowak, Werner Georg},
  Journal                  = {The Ramanujan Journal},
  Year                     = {1998},
  Number                   = {4},
  Pages                    = {421--440},
  Volume                   = {2},
  Doi                      = {10.1023/A:1009791425210},
  ISSN                     = {1382-4090},
  Keywords                 = {differences of powers; lattice points; exponential sums},
  Language                 = {English},
  Publisher                = {Kluwer Academic Publishers},
  Timestamp                = {2014.12.08},
  Url                      = {http://dx.doi.org/10.1023/A%3A1009791425210}}

@BOOK{bourbaki1987elements,
      TITLE = {Elements of mathematics: Topological vector spaces},
     AUTHOR = {Bourbaki, Nicolas and Eggleston, H.G. and Madan, S.},
       YEAR = {1987},
  PUBLISHER = {Springer-Verlag}}

@BOOK{rudin1991functional,
      TITLE = {Functional Analysis},
     AUTHOR = {Rudin, Walter},
       YEAR = {1991},
  edition = 	 {2nd},
  PUBLISHER = {New York, McGraw-Hill}}

@BOOK{atiyah1969introduction,
      TITLE = {Introduction to Commutative Algebra},
     AUTHOR = {Atiyah, Michael Francis and Macdonald, Ian Grant},
     VOLUME = {2},
       YEAR = {1969},
  PUBLISHER = {Addison-Wesley Reading}}

@book{fitzpatrick2007euclid,
  title={Euclid's Elements},
  author={Fitzpatrick, Richard},
  year={2007},
  publisher={Lulu.com},
  pages={98--99}}

@book{hartshorne2000geometry,
  title={Geometry: {E}uclid and beyond},
  author={Hartshorne, Robin},
  year={2000},
  publisher={Springer},
  pages={124}}


@book{efimov1981geometrie,
  title={G{\'e}om{\'e}trie sup{\'e}rieure},
  author={Efimov, Nikolai Vladimirovich},
  year={1981},
  publisher={Mir},
  pages={41--88}}

@book{linalgfischer:2002,
author={Fischer, Gerd},
title={Lineare Algebra},
edition={13},
publisher={Vieweg},
year={2002},
ADDRESS={Braunschweig, Wiesbaden}}

@book{analysisheuser:2003,
author={Heuser, Harro},
title={Lehrbuch der Analysis. {T}eil 1},
edition={15},
publisher={Teubner},
year={2003},
ADDRESS={Stuttgart, Leipzig, Wiesbaden}}

@book{bosch:2008,
author={Bosch, Siegfried},
title={Lineare Algebra},
edition={4},
publisher={Springer},
year={2008},
ADDRESS={Berlin, Heidelberg}}

@ARTICLE{LLL,
      AUTHOR  = {Lenstra, A. K. and Lenstra Jr., H. W. and Lov\'{a}sz, L.},
      TITLE   = {Factoring polynomials with rational coefficients},
      PUBLISHER={Springer-Verlag},
      JOURNAL = {Mathematische Annalen},
      pages = {515--534},
      doi = {10.1007/BF01457454},
      VOLUME = {261},
      NUMBER = {4}, 
      YEAR    = {1982}}  

@BOOK{LANDC,
      AUTHOR  = {Ebeling, Wolfgang},
      TITLE   = {Lattices and Codes},
      PUBLISHER={Springer Fachmedien Wiesbaden},
      SERIES = {Advanced Lectures in Mathematics},
      YEAR    = {2013}}

@BOOK{Jacobson2009,
AUTHOR  = {Jacobson, Nathan}, 
TITLE   = {Basic Algebra {I}}, 
SERIES = {2nd edition}, 
PUBLISHER={Dover {P}ublications {I}nc.}, 
YEAR    = {2009}}

@BOOK{Waerden2003,
AUTHOR  = {van der Waerden, B.L.}, 
TITLE   = {Algebra {I}}, 
SERIES = {4th edition}, 
PUBLISHER={Springer}, 
YEAR    = {2003}}

@BOOK{Luneburg1999,
AUTHOR  = {L\"{u}neburg, Heinz}, 
TITLE   = {Die grundlegenden Strukturen der {A}lgebra (in {G}erman)}, 
PUBLISHER={Oldenbourg Wisenschaftsverlag}, 
YEAR    = {1999}}

@BOOK{ReedSimon1972,
AUTHOR  = {Reed, Michael and Simon, Barry}, 
TITLE   = {Methods of modern mathematical physics},
SERIES = {Vol. 1}, 
PUBLISHER={Academic {P}ress, {N}ew {Y}ork}, 
YEAR    = {1972}}

@BOOK{Dax2002,
AUTHOR  = {Dax, Peter D.}, 
TITLE   = {Functional Analysis},
SERIES = {Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts}, 
PUBLISHER={Wiley Interscience}, 
YEAR    = {2002}}

@BOOK{Brezis2011,
AUTHOR  = {Brezis, Haim}, 
TITLE   = {Functional Analysis, Sobolev Spaces and Partial Differential Equations},
PUBLISHER={Springer}, 
YEAR    = {2011}}

@ARTICLE{BA1991,
  AUTHOR = {Biham, E. and Shamir, A.},
  TITLE = {Differential Cryptanalysis of {DES}-like Cryptosystems},
  JOURNAL = {Lecture Notes in Computer Science},
  VOLUME = {537},
  PAGES = {2--21},
  PUBLISHER = {Springer},
  YEAR = {1991}}

@ARTICLE{BA1993,
  AUTHOR = {Biham, E. and Shamir, A.},
  TITLE = {Differential Cryptanalysis of the Full 16-Round {DES}},
  JOURNAL = {Lecture Notes in Computer Science},
  VOLUME = {740},
  PAGES = {487--496},
  PUBLISHER = {Springer},
  YEAR = {1993}}

@BOOK{DuboisPrade:1980,
 AUTHOR={Dubois, Didier and Prade, Henri},
 TITLE={Fuzzy Sets and Systems: Theory and Applications},
 PUBLISHER={Academic Press, New York},
 YEAR=1980}

@ARTICLE{Zadeh:1965,
 AUTHOR={Zadeh, Lotfi},
 TITLE={Fuzzy sets},
 JOURNAL={Information and Control},
 YEAR=1965,
 VOLUME=8,
 NUMBER=3,
 PAGES={338--353}}

@ARTICLE{DuboisPrade:1978,
 AUTHOR={Dubois, Didier and Prade, Henri},
 TITLE={Operations on fuzzy numbers},
 JOURNAL={International Journal of System Sciences},
 YEAR=1978,
 VOLUME=9,
 NUMBER=6,
 PAGES={613--626}}

@ARTICLE{DuboisPrade:1990,
 AUTHOR={Dubois, Didier and Prade, Henri},
 TITLE={Rough fuzzy sets and fuzzy rough sets},
 JOURNAL={International Journal of General Systems},
 YEAR=1990,
 VOLUME=17,
 NUMBER={2-3},
 PAGES={191--209}}

@INPROCEEDINGS{GrabowskiFuzzy:2013,
AUTHOR = {Grabowski, Adam},
EDITOR = {Ganzha, M. and Maciaszek, L. and Paprzycki, M.},
TITLE = {On the Computer Certification of Fuzzy Numbers},
BOOKTITLE = {{2013 Federated Conference on Computer Science and Information Systems
(FedCSIS)}},
SERIES = {Federated Conference on Computer Science and Information Systems},
Year = {2013},
Pages = {51--54}}

@ARTICLE{GrabowskiFI:2014,
AUTHOR = {Grabowski, Adam},
TITLE = {Efficient Rough Set Theory Merging},
Journal = {Fundamenta Informaticae},
YEAR = {2014},
Volume = {135},
Number = {4},
Pages = {371--385},
DOI = {10.3233/FI-2014-1129}}

@book{rotman1995introduction,
  AUTHOR    = {Rotman, J.J.},
  TITLE     = {An Introduction to the Theory of Groups},
  PUBLISHER = {Springer},
  YEAR      = {1995}}

@book{robinson2012course,
  AUTHOR    = {Robinson, D.},
  TITLE     = {A Course in the Theory of Groups},
  PUBLISHER = {Springer New York},
  YEAR      = {2012}}

@ARTICLE{Lawvere:1963,
       AUTHOR = {Lawvere, F. William},
        TITLE = {Functorial Semantics of Algebraic Theories and
                 Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories},
      JOURNAL = {Reprints in Theory and Applications of Categories},
         YEAR = {2004},
       VOLUME = {5},
        PAGES = {1--121}}

@INPROCEEDINGS{GrabMo2004,
AUTHOR = {Grabowski, Adam and Moschner, Markus},
TITLE = {Managing Heterogeneous Theories within a Mathematical Knowledge Repository},
  booktitle     = {Mathematical Knowledge Management Proceedings},
  Note = {3rd International Conference on Mathematical Knowledge Management, Bialowieza, Poland, Sep. 19--21, 2004},
  pages     = {116--129},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3119},
  year      = {2004},
  DOI = {10.1007/978-3-540-27818-4_9},
  EDITOR = {Asperti, Andrea and Bancerek, Grzegorz and Trybulec, Andrzej}}

@ARTICLE{Wilf,
  AUTHOR =       {Wilf, Herbert S.},
  TITLE =        {Lectures on Integer Partitions},
  organization = {University of Pennsylvania},
  url = {http://www.math.upenn.edu/~wilf/PIMS/PIMSLectures.pdf}}

@BOOK{Andrews,
  AUTHOR =       {Andrews, George E. and Eriksson, Kimmo},
  TITLE =        {Integer Partitions},
  isbn =         {9780521600903}}

@BOOK{kolmogorov2012,
  TITLE      = {Elements of the Theory of Functions and Functional Analysis [Two Volumes in One]},
  AUTHOR     = {Kolmogorov, Andrey and Fomin, Sergei},
  PUBLISHER  = {Martino Fine Books},
  YEAR       = {2012}}

@book{bogachev2007measure,
  title={Measure theory},
  author={Bogachev, Vladimir Igorevich and Ruas, Maria Aparecida Soares},
  volume={1},
  year={2007},
  publisher={Springer}}

@book{aliprantis2006infinite,
  title={Infinite dimensional analysis},
  author={Aliprantis, Charalambos D., and Border, Kim C.},
  year={2006},
  publisher={Springer-Verlag, Berlin, Heidelberg}}

@BOOK{Rasiowa:2001,
 AUTHOR={Rasiowa, Helena},
 TITLE={Algebraic Models of Logics},
 PUBLISHER={Warsaw University},
 YEAR=2001}

@BOOK{RasiowaNonClassical,
 AUTHOR={Rasiowa, Helena},
 TITLE={An Algebraic Approach to Non-Classical Logics},
 PUBLISHER={North Holland},
 YEAR=1974}

@ARTICLE{Brignole,
 AUTHOR={Brignole, Diana},
 TITLE={Equational Characterization of {N}elson Algebra},
 JOURNAL={Notre Dame Journal of Formal Logic},
 YEAR=1969,
 VOLUME=X,
 NUMBER = 3,
 PAGES={285--297}}

@ARTICLE{RasiowaBirula,
 AUTHOR={Bia{\l}ynicki-Birula, Andrzej and Rasiowa, Helena},
 TITLE={On the Representation of Quasi-{B}oolean Algebras},
 JOURNAL={Bulletin de l'Academie Polonaise des Sciences},
 YEAR=1957,
 VOLUME=5,
 PAGES={259--261}}

@ARTICLE{Nelson,
 AUTHOR={Nelson, David},
 TITLE={Constructible Falsity},
 JOURNAL={Journal of Symbolic Logic},
 YEAR=1949,
 VOLUME=14,
 PAGES={16--26}}

@ARTICLE{GPH:2012,
 AUTHOR={Goli\'nska-Pilarek, Joanna and Huuskonen, Taneli},
 TITLE={Logic of Descriptions. {A} New Approach to
   the Foundations of Mathematics and Science},
 JOURNAL={Studies in Logic, Grammar and Rhetoric},
 NUMBER=27,
 VOLUME=40,
 PUBLISHER={University of Bia{\l}ystok},
 YEAR=2012}

@ARTICLE{Grzegorczyk:2012,
 AUTHOR={Grzegorczyk, Andrzej},
 TITLE={{F}ilozofia logiki i formalna {\sc logika niesymplifikacyjna}},
 JOURNAL={Zagadnienia Naukoznawstwa},
 NUMBER=4,
 NOTE={In Polish},
 VOLUME={XLVII},
 YEAR=2012}

@inproceedings{donolato2013vector,
title={A Vector-based Proof of {M}orley's Trisector Theorem},
author={Donolato, Cesare},
booktitle={Forum Geometricorum},
volume={13},
pages={233--235},
year={2013}}

@book{maor2014beautiful,
title={Beautiful geometry},
author={Maor, Eli and Jost, Eugen},
year={2014},
publisher={Princeton University Press}}

@article{MAI1,
year={2014},
issn={0343-6993},
journal={The Mathematical Intelligencer},
volume={36},
number={3},
doi={10.1007/s00283-014-9463-3},
title={On {M}orley's Trisector Theorem},
url={http://dx.doi.org/10.1007/s00283-014-9463-3},
publisher={Springer},
author={Conway, John},
pages={3},
language={English}}

@article{MAI2,
year={2014},
issn={0343-6993},
journal={The Mathematical Intelligencer},
volume={36},
number={3},
doi={10.1007/s00283-014-9481-1},
title={Is {J}ohn {C}onway's Proof of {M}orley's Theorem the Simplest and Free of {A} {D}eus {E}x {M}achina ?},
url={http://dx.doi.org/10.1007/s00283-014-9481-1},
publisher={Springer},
author={Karamzadeh, O.A.S.},
pages={4--7},
language={English}}

@article{connes1998new,
title={A new proof of {M}orley's theorem},
author={Connes, Alain},
journal={Publications Math{\'e}matiques de l'IH{\'E}S},
volume={88},
pages={43--46},
year={1998}}

@article{stonebridge2009simple,
title={A simple geometric proof of {M}orley's trisector theorem},
author={Stonebridge, Brian},
journal={Applied Probability Trust},
year={2009}}

@article{oakley1978morley,
title={The {M}orley trisector theorem},
author={Oakley, Cletus O. and Baker, Justine C.},
journal={American Mathematical Monthly},
pages={737--745},
year={1978},
publisher={A.M.S.}}

@article{letac,
title={Solutions ({M}orley's triangle). {P}roblem {N} 490},
author={Letac, A.},
journal={Sphinx: revue mensuelle des questions r\'ecr\'eatives}, 
publisher = {Brussels},
volume={9},
year = {1939}}

@article{CTK,
  title = {Morley's Miracle from Interactive Mathematics Miscellany and Puzzles},
  journal = {Cut the Knot},
  author={Bogomolny, Alexander},
  url = {http://www.cut-the-knot.org/triangle/Morley/index.shtml},
  year = 2015}

@incollection{NC2012,
year={2012},
isbn={978-1-4471-2729-1},
booktitle={Finitely Generated {A}belian Groups and Similarity of Matrices over a Field},
series={Springer Undergraduate Mathematics Series},
doi={10.1007/978-1-4471-2730-7_2},
title={Basic Theory of Additive {A}belian Groups},
url={http://dx.doi.org/10.1007/978-1-4471-2730-7_2},
publisher={Springer},
author={Norman, Christopher},
pages={47--96},
language={English}}

@incollection{holzl2013type,
  title={Type classes and filters for mathematical analysis in {I}sabelle/{HOL}},
  author={H{\"o}lzl, Johannes and Immler, Fabian and Huffman, Brian},
  booktitle={Interactive Theorem Proving},
  pages={279--294},
  year={2013},
  publisher={Springer}}

@article{boldo2014formalization,
  title={Formalization of real analysis: a survey of proof assistants and libraries},
  author={Boldo, Sylvie and Lelay, Catherine and Melquiond, Guillaume},
  journal={Mathematical Structures in Computer Science},
  pages={1--38},
  year={2014},
  publisher={Cambridge Univ. Press}}

@book{blahut2014cryptography,
  title={Cryptography and Secure Communication},
  author={Blahut, Richard E.},
  year={2014},
  publisher={Cambridge University Press}}

@book{inui2012group,
  title={Group theory and its applications in physics},
  author={Inui, Teturo and Tanabe, Yukito and Onodera, Yositaka},
  volume={78},
  year={2012},
  publisher={Springer Science and Business Media}}

@book{hewitt2012abstract,
  title={Abstract Harmonic Analysis: Volume {I}. Structure of Topological Groups. Integration. Theory Group Representations},
  author={Hewitt, Edwin and Ross, Kenneth A.},
  volume={115},
  year={2012},
  publisher={Springer Science and Business Media}}

@book{bourbaki2013general,
  title={General Topology: Chapters 1--4},
  author={Bourbaki, Nicolas},
  year={2013},
  publisher={Springer Science and Business Media}}

@INPROCEEDINGS{GPH:2015,
 AUTHOR={Goli\'nska-Pilarek, Joanna and Huuskonen, Taneli},
 EDITOR={Rafa{\l} Urbaniak and Gillman Payette},
 TITLE={Grzegorczyk's Non-{F}regean Logics},
 BOOKTITLE={Applications of Formal Philosophy: The Road Less Travelled},
 SERIES={Logic, Reasoning and Argumentation},
 PUBLISHER={Springer},
 YEAR={2015}}

@INPROCEEDINGS{Lukasiewicz:1931,
 AUTHOR={{\L}ukasiewicz, Jan},
 TITLE={Uwagi o aksjomacie {N}icoda i `dedukcji uog\'{o}lniaj\k{a}cej'},
 BOOKTITLE={Ksi\k{e}ga pami\k{a}tkowa {P}olskiego {T}owarzystwa {F}ilozoficznego},
 ADDRESS={Lw\'{o}w},
 YEAR={1931},
 NOTE = {In Polish}}

@ARTICLE{Suszko:1968,
 AUTHOR               = {Suszko, Roman},
 JOURNAL              = {Analele Universitatii Bucuresti. Acta Logica},
 PAGES                = {105--125},
 TITLE                = {Non-{F}regean logic and theories},
 VOLUME               = {9},
 YEAR                 = {1968}}

@ARTICLE{Suszko:1971,
 AUTHOR               = {Suszko, Roman},
 JOURNAL              = {Studia Logica},
 PAGES                = {77--81},
 TITLE                = {Semantics for the sentential calculus with identity},
 VOLUME               = {28},
 YEAR                 = {1971}}

@ARTICLE{BrignoleI:1967,
AUTHOR = {Brignole, Diana and Monteiro, Antonio},
TITLE = {Caracterisation des alg\`ebres de {N}elson par des egalit\'es, {I}},
JOURNAL = {Proceedings of the Japan Academy},
VOLUME = {43},
NUMBER = {4},
PAGES = {279--283},
YEAR = {1967},
doi = {10.3792/pja/1195521624}}

@ARTICLE{BrignoleII:1967,
AUTHOR = {Brignole, Diana and Monteiro, Antonio},
TITLE = {Caracterisation des alg\`ebres de {N}elson par des egalit\'es, {II}},
JOURNAL = {Proceedings of the Japan Academy},
VOLUME = {43},
NUMBER = {4},
PAGES = {284--285},
YEAR = {1967},
doi = {10.3792/pja/1195521625}}

@ARTICLE{GrabowskiJAR40,
AUTHOR = {Grabowski, Adam},
TITLE = {Mechanizing Complemented Lattices Within {M}izar System},
JOURNAL = {Journal of Automated Reasoning},
YEAR = {2015},
DOI = {10.1007/s10817-015-9333-5},
VOLUME = {55},
ISSUE = {3},
PAGES = {211--221}}

@article{cartan1937a,
title={Th\'eorie des filtres},
author={Cartan, Henri},
journal={C. R. Acad. Sci.},
volume={CCV},
year={1937},
pages={595--598}}

@book{wagschal,
title={Topologie et analyse fonctionnelle},
author={Wagschal, Claude},
publisher={Hermann},
year={1995}}

@BOOK{KleinbergTardos2005,
      AUTHOR = {Kleinberg, Jon  and Tardos, Eva},
      TITLE = {Algorithm Design},
      PUBLISHER = {Addison-Wesley},
      YEAR = {2005}}

@article{sierpinski1950,
title={Teoria liczb},
author={Sierpi{\'n}ski, Wac{\l}aw},
year={1950},
publisher={Instytut Matematyczny Polskiej Akademii Nauk},
NOTE = {In Polish}}

@misc{sierpinski1956,
title={O rozwi\k{a}zywaniu rowna{\'n} w liczbach ca{\l}kowitych},
author={Sierpi{\'n}ski, Wac{\l}aw},
year={1956},
publisher={P.W.N.},
NOTE = {In Polish}}

@book{gancarzewicz2000,
title={Arytmetyka},
author={Gancarzewicz, Jacek},
year={2000},
publisher={Wydawnictwo UJ, Krak{\'o}w},
NOTE = {In Polish}}

@article{caminati2013custom,
  title={Custom Automations in {M}izar},
  author={Caminati, Marco B. and Rosolini, Giuseppe},
  journal={Journal of Automated Reasoning},
  volume={50},
  number={2},
  pages={147--160},
  year={2013},
  publisher={Springer}}

@article{kornilowicz2013rewriting,
  title={On Rewriting Rules in {M}izar},
  author={Korni{\l}owicz, Artur},
  journal={Journal of Automated Reasoning},
  volume={50},
  number={2},
  pages={203--210},
  year={2013},
  publisher={Springer}}

@BOOK{FOLLAND,
  AUTHOR={Folland, Gerald B.},
  TITLE={Real Analysis: Modern Techniques and Their Applications},
  PUBLISHER={Wiley},
  YEAR={1999},
  EDITION={2nd}}

@BOOK{GARLING:1,
  AUTHOR={Garling, D.J.H.},
  TITLE={A Course in Mathematical Analysis: Volume 1, {F}oundations and Elementary Real Analysis},
  PUBLISHER={Cambridge University Press},
  YEAR={2013},
  VOLUME={1}}

@BOOK{Knuth1997,
      AUTHOR = {Knuth, Donald E.},
      TITLE = {The Art of Computer Programming, {V}olume 1: {F}undamental Algorithms, Third Edition},
      PUBLISHER = {Addison-Wesley},
      YEAR = {1997}}

@BOOK{Barbeau2003,
      AUTHOR = {Barbeau, E.J.},
      TITLE = {Polynomials},
      PUBLISHER = {Springer},
      YEAR = {2003}}

@book{bourbaki2007topologie,
  title={Topologie g{\'e}n{\'e}rale: Chapitres 1 {\`a} 4},
  author={Bourbaki, Nicolas},
  series={El{\'e}ments de math{\'e}matique},
  year={2007},
  publisher={Springer Science {\&} Business Media}}

@incollection{Mizar-State-2015,
year={2015},
isbn={978-3-319-20614-1},
booktitle={Intelligent Computer Mathematics},
volume={9150},
series={Lecture Notes in Computer Science},
editor={Kerber, Manfred and Carette, Jacques and Kaliszyk, Cezary and Rabe, Florian and Sorge, Volker},
doi={10.1007/978-3-319-20615-8_17},
title={Mizar: State-of-the-art and Beyond},
url={http://dx.doi.org/10.1007/978-3-319-20615-8_17},
publisher={Springer International Publishing},
author={Bancerek, Grzegorz and Byli{\'n}ski, Czes{\l}aw and Grabowski, Adam and Korni{\l}owicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P\k{a}k, Karol and Urban, Josef},
pages={261--279},
language={English}}

@ARTICLE{Jarvinen:2007,
  AUTHOR = {J\"arvinen, Jouni},
  TITLE = {Lattice Theory for Rough Sets},
  JOURNAL = {Transactions of Rough Sets, {VI}, Lecture Notes in Computer
  Science},
  VOLUME = 4374,
  YEAR = 2007,
  PAGES = {400--498}}

@ARTICLE{Gratzer:1957,
  AUTHOR = {Gr\"atzer, George and Schmidt, E.T.},
  TITLE = {On a problem of {M}.{H}. {S}tone},
  JOURNAL = {Acta Mathematica Academiae Scientarum Hungaricae},
  NUMBER = {8},
  YEAR = 1957,
  PAGES = {455--460}}

@inproceedings{GrabowskiPerspective:2007,
  author    = {Grabowski, Adam and Jastrz\k{e}bska, Magdalena},
  title     = {Rough Set Theory from a~Math-Assistant Perspective},
  booktitle = {Rough Sets and Intelligent Systems Paradigms, International Conference,
               {RSEISP} 2007, Warsaw, Poland, June 28--30, 2007, Proceedings},
  pages     = {152--161},
  year      = {2007},
  url       = {http://dx.doi.org/10.1007/978-3-540-73451-2_17},
  doi       = {10.1007/978-3-540-73451-2_17}}

@inproceedings{GrabowskiAssisted:2005,
 author = {Grabowski, Adam},
 title = {On the Computer-Assisted Reasoning About Rough Sets},
 booktitle = {International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location},
 series = {Advances in Soft Computing},
 volume = {28},
 editor = {Dunin-K\c{e}plicz, B. and Jankowski, A. and Skowron, A. and Szczuka, M.},
 location = {P{\l}ock, Poland, June 07--09, 2004},
 year = {2005},
 pages = {215--226},
 url = {http://dx.doi.org/10.1007/3-540-32370-8_15},
 doi = {10.1007/3-540-32370-8_15},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg}}

@BOOK{Bogachev2006,
  AUTHOR={Bogachev, V.I.},
  TITLE={Measure Theory},
  PUBLISHER={Springer},
  YEAR={2006},
  VOLUME={1}}

@BOOK{Rao2004,
  AUTHOR={Rao, M.M.},
  TITLE={Measure Theory and Integration},
  PUBLISHER={Marcel Dekker},
  YEAR={2004},
  EDITION={2nd}}

@ARTICLE{Peterson1981,
  author = {Peterson, G.},
  title = {Myths about the mutual exclusion problem},
  journal = {Information Processing Letters},
  year = {1981},
  volume = {12},
  pages = {1133--1145}}

@ARTICLE{Pratt1986,
  author = {Pratt, V.},
  title = {Modeling concurrency with partial orders},
  journal = {International Journal of Parallel Programming},
  year = {1986},
  volume = {15},
  pages = {33--71}}

@BOOK{chandy1988,
  title = {Parallel Program Design: A Foundation},
  publisher = {Addison Wesley},
  year = {1988},
  author = {Chandy, K. and Misra, J.}}

@ARTICLE{raynal991,
  author = {Raynal, M.},
  title = {A simple taxonomy for distributed mutual exclusion algorithms},
  journal = {ACM SIGOPS Operating Systems Review},
  year = {1991},
  volume = {25},
  pages = {47--50}}

@inproceedings{AbrIvNikitch2011,
  author = {Abraham, Uri and Ivanov, Ievgen and Nikitchenko, Mykola},
  title = {Proving behavioral properties of distributed algorithms using their compositional semantics},
  booktitle = {Proceedings of the First International Seminar Specification and Verification of Hybrid Systems, October 10-12, 2011, Taras Shevchenko National University of Kyiv},
  year = {2011},
  pages = {9--19}}

@incollection{IvanovNikitchAbr2014,
year={2014},
isbn={978-3-319-13205-1},
booktitle={Information and Communication Technologies in Education, Research, and Industrial Applications},
volume={469},
series={Communications in Computer and Information Science},
editor={Ermolayev, Vadim and Mayr, Heinrich C. and Nikitchenko, Mykola and Spivakovsky, Aleksander and Zholtkevych, Grygoriy},
doi={10.1007/978-3-319-13206-8_4},
title={On a Decidable Formal Theory for Abstract Continuous-Time Dynamical Systems},
url={http://dx.doi.org/10.1007/978-3-319-13206-8_4},
publisher={Springer International Publishing},
author={Ivanov, Ievgen and Nikitchenko, Mykola and Abraham, Uri},
pages={78--99}}

@ARTICLE{Abraham2011,
  author = {Abraham, Uri},
  title = {Logical Classification of Distributed Algorithms ({B}akery Algorithms
	as an example)},
  journal = {Theoretical Computer Science},
  year = {2011},
  volume = {412},
  pages = {2724--2745}}

@BOOK{Abraham1999,
  title = {Models for Concurrency},
  publisher = {Gordon and Breach},
  year = {1999},
  author = {Abraham, Uri}}

@ARTICLE{Abraham1995,
  author = {Abraham, Uri},
  title = {On Interprocess Communication and the Implementation of Multi-Writer
	Atomic Registers},
  journal = {Theoretical Computer Science},
  year = {1995},
  volume = {149},
  pages = {257--298}}

@ARTICLE{lamport1986,
  author = {Lamport, L.},
  title = {On interprocess communication. {P}art {I}: {B}asic formalism; {P}art {II}:
	{A}lgorithms},
  journal = {Distributed Computing},
  year = {1986},
  volume = {1},
  pages = {77--101}}

@MISC{Ridge2006,
    author = {Ridge, Tom},
    title = {Peterson's Algorithm in {I}sabelle/{HOL}},
    note = {\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.3484}},
    year = {2006}}

@incollection{Ridge2007,
year={2007},
isbn={978-3-540-74590-7},
booktitle={Theorem Proving in Higher Order Logics},
volume={4732},
series={Lecture Notes in Computer Science},
editor={Schneider, Klaus and Brandt, Jens},
doi={10.1007/978-3-540-74591-4_21},
title={Operational Reasoning for Concurrent {C}aml Programs and Weak Memory Models},
url={http://dx.doi.org/10.1007/978-3-540-74591-4_21},
publisher={Springer Berlin Heidelberg},
author={Ridge, Tom},
pages={278--293}}

@BOOK{GOLDREICH,
      AUTHOR = {Goldreich, Oded},
      TITLE = {Foundations of Cryptography: Volume 1, {B}asic Tools},
      PUBLISHER = {Cambridge University Press},
      YEAR = {2001}}

@MISC{BELLARE,
 AUTHOR={Bellare, Mihir},
 TITLE={A Note on Negligible Functions},
 INSTITUTION={University of California at San Diego},
 YEAR=2002}

@BOOK{Bauer:2002,
  AUTHOR={Bauer, Heinz},
  TITLE={Measure and Integration Theory},
  PUBLISHER={Walter de Gruyter Inc.},
  YEAR={2002}}

@article{biagini-rost:2012,
author={Biagini, Francesca and Rost, Daniel},
title={Money out of nothing? – {P}rinzipien und Grundlagen der Finanzmathematik},
publisher={de Gruyter},
  journal = {Mitteilungen der {D}eutschen {M}athematiker-{V}ereinigung},
  year = {2013},
  volume = {21},
  NUMBER = {1},
  pages = {18--22},
 doi = {10.1515/dmvm-2013-0011}}

@book{kremer:2006,
  author={Kremer, J\"{u}rgen},
  title={Einf\"{u}hrung in die diskrete Finanzmathematik},
  publisher={Springer-Verlag},
  year={2006},
  ADDRESS={Berlin, Heidelberg, New York}}

@book{sandmann:2001,
  author={Sandmann, Klaus},
  title={Einf\"{u}hrung in die Stochastik der Finanzm\"{a}rkte},
  edition={2},
  publisher={Springer-Verlag},
  year={2001},
  ADDRESS={Berlin, Heidelberg, New York}}

@Article{JouannaudLescanne,
  author = 	 {Jouannaud, Jean-Pierre and Lescanne, Pierre},
  title = 	 {On Multiset Ordering},
  journal = 	 {Information Processing Letters},
  year = 	 {1982},
  volume =	 {15},
  number =	 {2},
  pages =	 {57--63},
  doi = 	 {10.1016/0020-0190(82)90107-7}}

@BOOK{campbell1956trigonometrie,
  title={La trigonom{\'e}trie},
  author={Campbell, R.},
  series={Que sais-je?},
  year={1956},
  publisher={Presses universitaires de France}}

@article{Maurey2005,
author = {Maurey, Bernard and Tacchi, Jean-Pierre},
journal = {Revue d'histoire des math{\'e}matiques},
number = {2},
pages = {163--204},
publisher = {Soci{\'e}t{\'e} math{\'e}matique de France},
title = {La gen{\`e}se du th{\'e}or{\`e}me de recouvrement de {B}orel},
url = {http://eudml.org/doc/252094},
volume = {11},
year = {2005}}

@article{Cousin1895,
year={1895},
issn={0001-5962},
journal={Acta Mathematica},
volume={19},
number={1},
doi={10.1007/BF02402869},
title={Sur les fonctions de $n$ variables complexes},
url={http://dx.doi.org/10.1007/BF02402869},
publisher={Kluwer Academic Publishers},
author={Cousin, Pierre},
pages={1--61},
language={French}}

@article{Raman2015,
     title = {A Pedagogical History of Compactness},
     author = {Raman-Sundstr{\"o}m, Manya},
     journal = {The American Mathematical Monthly},
     volume = {122},
     number = {7},
     pages = {619--635},
     url = {http://www.jstor.org/stable/10.4169/amer.math.monthly.122.7.619},
     year = {2015},
     publisher = {Mathematical Association of America}}

@book{yee2000integral,
  title={Integral: an easy approach after {K}urzweil and {H}enstock},
  author={Yee, Lee Peng and Vyborny, Rudolf},
  volume={14},
  year={2000},
  publisher={Cambridge University Press}}

@article{bartle1996return,
  title={Return to the {R}iemann integral},
  author={Bartle, Robert G.},
  journal={American Mathematical Monthly},
  pages={625--632},
  year={1996},
  publisher={JSTOR}}

@book{bartle2001modern,
  title={A modern theory of integration},
  author={Bartle, Robert G.},
  volume={32},
  year={2001},
  publisher={American Mathematical Society Providence}}

@article{peng2008integral,
  title={The integral {\`a} la {H}enstock},
  author={Yee, Lee Peng},
  journal={Scientiae Mathematicae Japonicae},
  volume={67},
  number={1},
  pages={13--21},
  year={2008}}

@article{mawhin2001eternel,
  title={L'{\'e}ternel retour des sommes de {R}iemann-{S}tieltjes dans l'{\'e}volution du calcul int{\'e}gral},
  author={Mawhin, Jean},
  journal={Bulletin de la Soci{\'e}t{\'e} Royale des Sciences de Li{\`e}ge},
  volume={70},
  number={4--6},
  pages={345--364},
  year={2001},
  publisher={Soci{\'e}t{\'e} Royale des Sciences de Li{\`e}ge}}

@book{mawhin1992analyse,
  title={Analyse: fondements, techniques, {\'e}volution},
  author={Mawhin, Jean},
  year={1992},
  publisher={De Boeck}}

@BOOKLET{SchmetsAM:2004,
TITLE = {Analyse Math{\Že}matique},
AUTHOR = {Schmets, Jean},
HOWPUBLISHED = {Notes de cours, Universit{\'e} de Li{\`e}ge, 337 pages},
YEAR = {2004},
LANGUAGE={French},
url = {http://www.anmath.ulg.ac.be/js/ens/am.pdf}}

@book{deza2009encyclopedia,
  title={Encyclopedia of distances},
  author={Deza, Michel Marie and Deza, Elena},
  year={2009},
  publisher={Springer}}

@article{caratheodorycommunity:2004,
author={Biagini, Francesca and Rost, Daniel},
title={Money out of nothing? - {P}rinzipien und {G}rundlagen der {F}inanzmathematik},
journal={MATHE-LMU.DE},
volume={LMU-M{\"u}nchen},
number={25},
pages={28--34},
year={2012},
url={https://caratheodory-gesellschaft-lmu.de/content/03-zeitschrift/ausgabe25.pdf}}

@Inbook{Erdos2003,
author={Erd{\H{o}}s, Paul and Sur{\'a}nyi, J{\'a}nos},
chapter={Divisibility, the {F}undamental {T}heorem of {N}umber {T}heory},
title={Topics in the Theory of Numbers},
year={2003},
publisher={Springer New York},
pages={1--37},
doi={10.1007/978-1-4613-0015-1_1},
url={http://dx.doi.org/10.1007/978-1-4613-0015-1_1}}

@BOOK{Stroock1999,
  TITLE = {A Concise Introduction to the Theory of Integration},
  AUTHOR = {Stroock, Daniel W.},
  PUBLISHER = {Springer Science \& Business Media},
  YEAR  = {1999}}

@BOOK{Kestelman1960,
  TITLE={Modern theories of integration},
  AUTHOR={Kestelman, H.},
  PUBLISHER={Dover Publications},
  YEAR={1960},
  EDITION={2nd}}

@BOOK{Gupta1986,
  TITLE = {Fundamental Real Analysis},
  AUTHOR = {Gupta, S.L. and Rani, Nisha},
  PUBLISHER = {Vikas Pub.},
  YEAR = {1986}}

@BOOK{Hille1974,
  TITLE={Methods in classical and functional analysis},
  AUTHOR={Hille, Einar},
  PUBLISHER={Addison-Wesley Publishing Co., Halsted Press},
  YEAR={1974}}

@Article{DershowitzTCS,
  author = 	 {Dershowitz, Nachum},
  title = 	 {Orderings for term-rewriting systems},
  journal = 	 {Theoretical Computer Science},
  year = 	 {1982},
  volume =	 {17},
  number =	 {3},
  pages =	 {279--301},
  doi = 	 {10.1016/0304-3975(82)90026-3}}
  
@Article{DershowitzManna1979,
  author = 	 {Dershowitz, Nachum and Manna, Zohar},
  title = 	 {Proving Termination with Multiset Orderings},
  journal = 	 {Communications of the ACM},
  year = 	 {1979},
  volume =	 {22},
  number =	 {8},
  pages =	 {465--476},
  doi = 	 {10.1145/359138.359142}}  
  
 @techreport{HuetOppen1980,
 author = {Huet, Gerard and Oppen, Derek C.},
 title = {Equations and Rewrite Rules: A Survey},
 year = {1980},
 url = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Astan%3ASTAN%2F%2FCS-TR-80-785},
 publisher = {Stanford University},
 address = {Stanford, CA, USA}} 

@Article{FourDecades,
author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
title={Four Decades of {M}izar},
journal={Journal of Automated Reasoning},
year={2015},
volume={55},
number={3},
pages={191--198},
issn={1573-0670},
doi={10.1007/s10817-015-9345-1}}

@inproceedings{GrabowskiFed2016,
  author    = {Grabowski, Adam},
  title     = {Tarski's geometry modelled in {M}izar computerized proof assistant},
  booktitle = {Proceedings of the 2016 Federated Conference on Computer Science and
               Information Systems, FedCSIS 2016, Gda{\'{n}}sk, Poland, September
               11--14, 2016},
  editors = {Ganzha, Maria and Maciaszek, Leszek and Paprzycki, Marcin},
  pages     = {373--381},
  year      = {2016},
  doi       = {10.15439/2016F290}}

@inproceedings{Makarios,
author = {Makarios, Timothy James McKenzie},
title = {A mechanical verification of the independence of {T}arski's {E}uclidean
{A}xiom},
note = {Master's thesis},
url={https://books.google.be/books?id=76J2MwEACAAJ},
publisher={Victoria University of Wellington, New Zealand},
year = 2012}

@inproceedings{GrabowskiDuplication,
  author    = {Grabowski, Adam and Schwarzweller, Christoph},
  title     = {On Duplication in Mathematical Repositories},
  booktitle = {Intelligent Computer Mathematics, 10th International Conference, {AISC}
               2010, 17th Symposium, Calculemus 2010, and 9th International Conference,
               {MKM} 2010, Paris, France, July 5--10, 2010. Proceedings},
  pages     = {300--314},
  year      = {2010},
  editor    = {Serge Autexier and
               Jacques Calmet and
               David Delahaye and
               Patrick D. F. Ion and
               Laurence Rideau and
               Renaud Rioboo and
               Alan P. Sexton},
  series    = {Lecture Notes in Computer Science},
  volume    = {6167},
  publisher = {Springer},
  doi       = {10.1007/978-3-642-14128-7_26}}

@incollection{vlach2008topologies,
  title={Topologies of Approximation Spaces of Rough Set Theory},
  author={Vlach, Milan},
  booktitle={Interval/Probabilistic Uncertainty and Non-Classical Logics},
  pages={176--186},
  year={2008},
  publisher={Springer}}

@inproceedings{vlach2008algebraic,
  title={Algebraic and Topological Aspects of Rough Set Theory},
  author={Vlach, Milan},
  booktitle={Fourth International Workshop on Computational Intelligence \& Applications,
  IEEE SMC Hiroshima Chapter, Hiroshima University, Japan, December 10\&11},
  year={2008}}

@incollection{gehrke2010topological,
  title={A Topological Approach to Recognition},
  author={Gehrke, Mai and Grigorieff, Serge and Pin, Jean-{\'E}ric},
  booktitle={Automata, Languages and Programming},
  pages={151--162},
  year={2010},
  publisher={Springer}}

@article{pervin1962quasi,
  title={Quasi-Uniformization of Topological Spaces},
   author={Pervin, William J.},
   journal={Mathematische Annalen},
   volume={147},
   number={4},
   pages={316--317},
   year={1962},
   publisher={Springer}}

 @article{kunzi2009introduction,
   title={An Introduction to Quasi-Uniform Spaces},
   author={K{\"u}nzi, Hans-Peter A.},
   journal={Beyond Topology},
   volume={486},
   pages={239--304},
   year={2009},
   publisher={Amer. Math. Soc.}}

@inproceedings{kunzi1995bourbaki,
   title={The {B}ourbaki Quasi-Uniformity},
   author={K{\"u}nzi, Hans-Peter A. and Ryser, Carolina},
   booktitle={Topology Proceedings},
   volume={20},
   pages={161--183},
   year={1995}}

@inproceedings{kunzi1993quasi,
   title={Quasi-Uniform Spaces - Eleven Years Later},
   author={K{\"u}nzi, Hans-Peter A.},
   booktitle={Topology Proceedings},
   volume={18},
   pages={143--171},
   year={1993}}

 @article{williams1972locally,
   title={Locally Uniform Spaces},
   author={Williams, James},
   journal={Transactions of the American Mathematical Society},
   volume={168},
   pages={435--469},
   year={1972}}

@article{Naumowicz2006396,
title = {An example of formalizing recent mathematical results in {M}izar},
journal = {Journal of Applied Logic},
volume = {4},
number = {4},
pages = {396--413},
year = {2006},
note = {Towards Computer Aided Mathematics},
issn = {1570-8683},
doi = {10.1016/j.jal.2005.10.003},
url = {http://www.sciencedirect.com/science/article/pii/S1570868305000686},
author = {Naumowicz, Adam}}

@BOOK{WE2009,
      AUTHOR = {Weintraub, Steven H.},
      TITLE = {Galois Theory},
      EDITION = {2},
      PUBLISHER = {Springer-Verlag},
      YEAR = {2009}}

@book{wagschaltopex,
title={Topologie: Exercices et probl{\`e}mes corrig{\'e}s},
author={Wagschal, Claude},
publisher={Hermann},
year={1995}}

@BOOK{Kreyszig1989,
  title={Introductory Functional Analysis with Applications},
  author={Kreyszig, Erwin},
  publisher={Wiley},
  year={1989},
  edition={1}}

@book {Niven1956,
    AUTHOR = {Niven, Ivan},
     TITLE = {Irrational numbers},
    SERIES = {The Carus Mathematical Monographs, No. 11},
 PUBLISHER = {The Mathematical Association of America. Distributed by John
              Wiley and Sons, Inc., New York, N.Y.},
      YEAR = {1956},
     PAGES = {37--41}}

@incollection{magaud2008formalizing,
  title={Formalizing projective plane geometry in {C}oq},
  author={Magaud, Nicolas and Narboux, Julien and Schreck, Pascal},
  booktitle={Automated Deduction in Geometry},
  pages={141--162},
  year={2008},
  publisher={Springer}}

@incollection{apel2010cancellation,
  title={Cancellation patterns in automatic geometric theorem proving},
  author={Apel, Susanne and Richter-Gebert, J{\"u}rgen},
  booktitle={Automated Deduction in Geometry},
  pages={1--33},
  year={2010},
  publisher={Springer}}

@book{apel2014phd,
  title={The geometry of brackets and the area principle},
  publisher={Phd thesis, Technische Universit{\"a}t M{\"u}nchen, Fakult{\"a}t f{\"u}r Mathematik},
  url={http://mediatum.ub.tum.de/node?id=1175107},
  year={2014},
  author={Apel, Susanne}}

@incollection{fuchs2010formalization,
  title={A formalization of {G}rassmann-{C}ayley algebra in {C}oq and its application to theorem proving in projective geometry},
  author={Fuchs, Laurent and Thery, Laurent},
  booktitle={Automated Deduction in Geometry},
  pages={51--67},
  year={2010},
  publisher={Springer}}

@article{richter1995mechanical,
  title={Mechanical theorem proving in projective geometry},
  author={Richter-Gebert, J{\"u}rgen},
  journal={Annals of Mathematics and Artificial Intelligence},
  volume={13},
  number={1-2},
  pages={139--172},
  year={1995},
  publisher={Springer}}

@book{richter2011perspectives,
  title={Perspectives on projective geometry: a guided tour through real and complex geometry},
  author={Richter-Gebert, J{\"u}rgen},
  year={2011},
  publisher={Springer Science \& Business Media}}

@BOOK{Knopp,
  AUTHOR =       {Knopp, Konrad},
  TITLE =        {Infinite Sequences and Series},
  YEAR={1956},
  PUBLISHER = {Dover Publications},
  URL = {https://pl.scribd.com/doc/180234043/Knopp-Infinite-Sequences-and-Series-1956-pdf},
  isbn =         {978-0-486-60153-3}}

@book{sawyer1970,
title={The Search for Pattern},
author={Sawyer, W.W.},
year={1970},
publisher={Penguin Books Ltd, Harmondsworth, Middlessex, England}}

@BOOK{AniWas,
AUTHOR={Wasilewska, Anita},
TITLE={An Introduction to Classical and Non-Classical Logics},
PUBLISHER={SUNY Stony Brook},
YEAR={2005}}

@BOOK{Zariski1975,
 AUTHOR={Zariski, Oscar and Samuel, Pierre},
 TITLE={Commutative Algebra {I}},
 edition={2nd},
 publisher={Springer},
 year={1975}}

@book{nagata1985,
  title={Theory of Commutative Fields},
  author={Nagata, Masayoshi},
  note ={Translations of Mathematical Monographs},
  volume = {125},
  year={1985},
  publisher={American Mathematical Society}}

@book{matsumura1989,
  title={Commutative Ring Theory},
  author={Matsumura, Hideyuki},
  note ={Cambridge Studies in Advanced Mathematics},
  year={1989},
  edition = {2nd},
  publisher={Cambridge University Press}}

@book{aar1999,
  title={Special Functions},
  author={Andrews, George E. and Askey, Richard and Roy, Ranjan},
  year={1999},
  publisher={Cambridge University Press}}

@book{debnath2010,
  title={The Legacy of {L}eonhard {E}uler: A Tricentennial Tribute},
  author={Debnath, Lokenath},
  year={2010},
  publisher={World Scientific}}

@Article{CAO201096,
  Title                    = {Factors of alternating binomial sums},
  Author                   = {Hui-Qin, Cao and Hao, Pan},
  Journal                  = {Advances in Applied Mathematics},
  Pages                    = {96--107},
  Volume                   = {45},
  Year                     = {2010},
  Number                   = {1},
  Doi                      = {http://dx.doi.org/10.1016/j.aam.2009.09.004},
  ISSN                     = {0196-8858},
  Url                      = {http://www.sciencedirect.com/science/article/pii/S0196885809001195}}

@Article{KHANDUJA2011300,
  Title                    = {Some irreducibility results for truncated binomial expansions},
  Author                   = {Khanduja, Sudesh K. and Khassa, Ramneek and Laishram, Shanta},
  Journal                  = {Journal of Number Theory},
  Pages                    = {300--308},
  Volume                   = {131},
  Year                     = {2011},
  Number                   = {2},
  Doi                      = {http://dx.doi.org/10.1016/j.jnt.2010.08.004},
  ISSN                     = {0022-314X},
  Url                      = {http://www.sciencedirect.com/science/article/pii/S0022314X10002271}}

@book{wp1994,
  title={Notions and theorems of elementary formal logic},
  author={Pogorzelski, Witold},
  year={1994},
  publisher={Wydawnictwo UwB, Bialystok}}

@book{wp1992,
  title={Dictionary of Formal Logic},
  author={Pogorzelski, Witold},
  year={1992},
  publisher={Wydawnictwo UwB, Bialystok}}

@Article{king2006,
  Title                    = {Integer roots of polynomials},
  Author                   = {King, J.D.},
  Journal                  = {The Mathematical Gazette},
  Pages                    = {455--456},
  Volume                   = {90},
  Year                     = {2006},
  Number                   = {519},
  Doi                      = {http://dx.doi.org/10.1017/S0025557200180295},
  Url                      = {https://www.cambridge.org/core/journals/mathematical-gazette/article/div-classtitle9063-integer-roots-of-polynomialsdiv/2AF0D61B7CFC1F3DC3F3625DA8CC0270}}

@ARTICLE{Liouville1844,
AUTHOR = {Liouville, Joseph},
TITLE = {Nouvelle d{\'e}monstration d'un th{\'e}or{\`e}me sur les irrationnelles alg{\'e}briques, ins{\'e}r{\'e} dans le {C}ompte {R}endu de la derni{\`e}re s{\'e}ance},
JOURNAL = {Compte Rendu Acad. Sci. Paris},
VOLUME = {S{\'e}r.A},
NUMBER = {18},
PAGES = {910--911},
YEAR = {1844}}

@article{Tarskis_Geometry-AFP,
  author  = {Makarios, Timothy James McKenzie},
  title   = {The independence of {T}arski's {E}uclidean {A}xiom},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2012,
  url     = {http://isa-afp.org/entries/Tarskis_Geometry.shtml},
  note    = {Formal proof development},
  ISSN    = {2150-914x}}

@BOOK{Pre84,
      AUTHOR = {Prestel, Alexander},
      TITLE = {Lectures on Formally Real Fields},
      PUBLISHER = {Springer-Verlag},
      YEAR = {1984}}

@BOOK{KS89,
      AUTHOR = {Knebusch, Manfred and Scheiderer, Claus},
      TITLE = {Einf\"{u}hrung in die reelle {A}lgebra},
      PUBLISHER = {Vieweg-Verlag},
      YEAR = {1989}}

@BOOK{Jac64,
      AUTHOR = {Jacobson, Nathan},
      TITLE = {Lecture Notes in Abstract Algebra, {III}. {T}heory of Fields and {G}alois Theory},
      PUBLISHER = {Springer-Verlag},
      YEAR = {1964}}

@BOOK{Rad91,
      AUTHOR = {Radbruch, Knut},
      TITLE = {Geordnete K\"{o}rper},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}

@BOOK{KURATOWSKI_RRC,
      AUTHOR = {Kuratowski, Kazimierz},
       TITLE = {Rachunek r{\'o}{\.z}niczkowy i ca{\l}kowy -- funkcje jednej zmiennej},
   PUBLISHER = {PWN -- Warszawa (in polish)},
      SERIES = {Biblioteka Matematyczna},
        YEAR = {1964}}

@inproceedings{GrabKornSchwarz:2016,
    Author = {Grabowski, Adam and Korni{\l}owicz, Artur and Schwarzweller, Christoph},
    Editor = {Ganzha, M. and Maciaszek, L. and Paprzycki, M.},
    Title = {On Algebraic Hierarchies in Mathematical Repository of {M}izar},
  Booktitle = {Proceedings of the 2016 {F}ederated {C}onference on {C}omputer {S}cience and {I}nformation {S}ystems (FedCSIS)},
  Series = {Annals of Computer Science and Information Systems},
  Year = {2016},
 Volume = {8},
 Pages = {363--371},
  DOI = {10.15439/2016F520}}

@BOOK{Conway:1996,
AUTHOR = {Conway, J.H. and Guy, R.K.},
TITLE = {The Book of Numbers},
publisher = {Springer-Verlag},
YEAR = {1996}}


@BOOK{Apostol:1997,
AUTHOR = {Apostol, Tom M.},
TITLE = {Modular Functions and {D}irichlet Series in Number Theory},
edition = {2nd},
publisher = {Springer-Verlag},
YEAR = {1997}}


@article{Bingham:2011,
  title={Formalizing a Proof that $e$ is Transcendental},
  author={Bingham, Jesse},
  journal={Journal of Formalized Reasoning},
  year={2011},
  volume={4},
  pages={71--84}}


@inproceedings{Bernard:2016,
  author = {Bernard, Sophie and Bertot, Yves and Rideau, Laurence and Strub, Pierre{-}Yves},
  booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs and Proofs},
  doi = {10.1145/2854065.2854072},
  editor = {Avigad, Jeremy and Chlipala, Adam},
  pages = {76--87},
  publisher = {ACM},
  title = {Formal proofs of transcendence for $e$ and $\pi$ as an application of multivariate and symmetric polynomials},
  year = {2016}}


@article{Eberl-AFP:2015,
  author  = {Eberl, Manuel},
  title   = {Liouville numbers},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Liouville_Numbers.shtml}, Formal proof development},
  ISSN    = {2150-914x}}

@BOOK{Klement:2000,
AUTHOR = {Klement, Erich Peter and Mesiar, Radko and Pap, Endre},
TITLE = {Triangular Norms},
PUBLISHER = {Dordrecht: Kluwer},
YEAR = {2000}}

@BOOK{Hajek:1998,
AUTHOR = {H\'ajek, Petr},
TITLE = {Metamathematics of Fuzzy Logic},
PUBLISHER = {Dordrecht: Kluwer},
YEAR = {1998}}

@inproceedings{rudnicki2011escape,
  title={Escape to {ATP} for {M}izar},
  author={Rudnicki, Piotr and Urban, Josef},
  booktitle={First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011},
  year={2011}}

@Inbook{Richter-Gebert2011,
author={Richter-Gebert, J{\"u}rgen},
title={Pappos's Theorem: Nine Proofs and Three Variations},
bookTitle={Perspectives on Projective Geometry: A Guided Tour Through Real and Complex Geometry},
year={2011},
publisher={Springer Berlin Heidelberg},
pages={3--31},
isbn={978-3-642-17286-1},
doi={10.1007/978-3-642-17286-1_1},
url={http://dx.doi.org/10.1007/978-3-642-17286-1_1}}

@article{alama2012escape,
  title={Escape to {M}izar for {ATP}s},
  author={Alama, Jesse},
  journal={arXiv preprint arXiv:1204.6615},
  year={2012}}

@BOOK{MSZ,
  AUTHOR = {Maschler, Michael and Solan, Eilon and Zamir, Shmuel},
  TITLE = {Game theory},
  ADRESS = {Cambridge [u.a.]},
  PUBLISHER = {Cambridge Univ. Press},
  YEAR = {2013},
  ISBN = {978-1-107-00548-8},
  DOI = {10.1017/CBO9780511794216},
  PAGES = {XXVI, 979 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?32611138_toc.pdf}}

@BOOK{OSI,
  AUTHOR={Schr{\"o}der, Bernd S.W.},
  TITLE={Ordered Sets: An Introduction},
  PUBLISHER={Birkh{\"a}user Boston},
  YEAR={2003},
  ISBN={978-1-4612-6591-7},
  note={\url{https://books.google.de/books?id=hg8GCAAAQBAJ}}}

@BOOK{IAlg,
AUTHOR = {Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L.},
TITLE = {Introduction to algorithms},
EDITOR= {Cormen, Thomas H.},
ADRESS = {Cambridge, Mass. [u.a.]},
PUBLISHER = {MIT Press},
YEAR = {2009},
EDITION = {3. ed.},
ISBN = {0-262-53305-7, 978-0-262-53305-8, 978-0-262-03384-8},
PAGES = {XIX, 1292 S.},
note = {\url{http://scans.hebis.de/HEBCGI/show.pl?21502893\_toc.pdf}}}

@book{Vinberg,
 author = {Vinberg, E. B.},
 title = {A {C}ourse in {A}lgebra},
 publisher = {American Mathematical Society},
 year = {2003},
 ISBN = {0821834134}}

@book{Cauchy1821,
 author = {Cauchy, Augustin Louis},
 title = {Cours d'analyse de l'{E}cole royale polytechnique},
 publisher = {de l'{I}mprimerie royale},
 year = {1821}}

@inproceedings{grabowski2006solving,
  author    = {Grabowski, Adam},
  title     = {Solving Two Problems in General Topology Via Types},
  booktitle = {Types for Proofs and Programs, International Workshop, {TYPES} 2004,
               Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers},
  pages     = {138--153},
  year      = {2004},
  crossref  = {DBLP:conf/types/2004},
  url       = {https://doi.org/10.1007/11617990_9},
  doi       = {10.1007/11617990_9},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  note    = {\url{http://dblp.uni-trier.de/rec/bib/conf/types/Grabowski04}},
  bibsource = {dblp computer science bibliography, http://dblp.org}}


@inproceedings{GrabowskiMitsuishi:2015,
  author    = {Grabowski, Adam and Mitsuishi, Takashi},
  title     = {Initial Comparison of Formal Approaches to Fuzzy and Rough Sets},
  booktitle = {Artificial Intelligence and Soft Computing - 14th International Conference,
               {ICAISC} 2015, Zakopane, Poland, June 14-18, 2015, Proceedings, Part {I}},
  pages     = {160--171},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-19324-3_15},
  doi       = {10.1007/978-3-319-19324-3_15},
  editor    = {Leszek Rutkowski and
               Marcin Korytkowski and
               Rafal Scherer and
               Ryszard Tadeusiewicz and
               Lotfi A. Zadeh and
               Jacek M. Zurada},
  series    = {Lecture Notes in Computer Science},
  volume    = {9119},
  publisher = {Springer}}

@article{Floyd1967,
 author = {Floyd, R.W.},
 journal = {Mathematical aspects of computer science},
 number = {19--32},
 title = {Assigning meanings to programs},
 volume = 19,
 year = 1967}

@article{Hoare1969,
 author    = {Hoare, C.A.R.},
 title     = {An Axiomatic Basis for Computer Programming},
 journal   = {Commun. {ACM}},
 volume    = {12},
 number    = {10},
 pages     = {576--580},
 year      = {1969}}

@article{Redko1979,
author={Red'ko, V.N.},
title={Backgrounds of compositional programming},
journal = {Programming [in Russian]},
number = {3},
year = {1979},
pages = {3--13}}

@ARTICLE{Redko1988,
 author = {Red'ko, V.N. and Nikitchenko, N.S.},
 title = {Composition aspects of programmology. \uppercase{II}},
 journal = {Cybernetics and Systems Analysis},
 year = {1988},
 volume = {24},
 pages = {33--41},
 number = {1},
 publisher = {Springer}}

@ARTICLE{Redko1987,
 author = {Red'ko, V.N. and Nikitchenko, N.S.},
 title = {Composition aspects of programmology. \uppercase{I}},
 journal = {Cybernetics and Systems Analysis},
 year = {1987},
 volume = {23},
 pages = {627--637},
 number = {5},
 publisher = {Springer}}

@TECHREPORT{Nikitch98,
 title={A Composition Nominative Approach to Program Semantics},
 author={Nikitchenko, Nikolaj S.},
 institution={Department of Information Technology, Technical University of Denmark},
 number={IT-TR 1998-020},
 year={1998}}

@book{NikitchShkilniak2008,
author = {Nikitchenko, M.S. and Shkilniak, S.S.},
title = {Mathematical logic and theory of algorithms},
publisher = {Publishing house of Taras Shevchenko National University of Kyiv, Ukraine (in Ukrainian)},
numpages = {528},
year = {2008}}

@book{NikitchShkilniak2013,
author = {Nikitchenko, M.S. and Shkilniak, S.S.},
title = {Applied logic},
publisher = {Publishing house of Taras Shevchenko National University of Kyiv, Ukraine (in Ukrainian)},
year = {2013}}

@inproceedings{Skobelev2014,
 author    = {Skobelev, Volodymyr G. and Nikitchenko, Mykola and Ivanov, Ievgen},
 title     = {On Algebraic Properties of Nominative Data and Functions},
 booktitle = {Information and Communication Technologies in Education, Research,
              and Industrial Applications -- 10th International Conference, {ICTERI}
              2014, Kherson, Ukraine, June 9--12, 2014, Revised Selected Papers},
 pages     = {117--138},
 year      = {2014},
 crossref  = {DBLP:conf/icteri/2014},
 url       = {https://doi.org/10.1007/978-3-319-13206-8_6},
 doi       = {10.1007/978-3-319-13206-8_6}}

@article{DBLP:journals/csjm/IvanovNS16,
 author    = {Ivanov, Ievgen and Nikitchenko, Mykola and Skobelev, Volodymyr G.},
 title     = {Proving Properties of Programs on Hierarchical Nominative Data},
 journal   = {The Computer Science Journal of Moldova},
 volume    = {24},
 number    = {3},
 pages     = {371--398},
 year      = {2016}}

@inproceedings{MizarNominative,
title = {Formalization of Nominative Data in {M}izar},
author = {Ivanov, Ievgen and Korni{\l}owicz, Artur and Nikitchenko, Mykola},
series = {Proceedings of TAAPSD 2015, 23--26 December 2015},
publisher = {Taras Shevchenko National University of Kyiv, Ukraine},
pages = {82--85},
year = {2015}}

@Inbook{Kryvolap2013,
author={Kryvolap, Andrii and Nikitchenko, Mykola and Schreiner, Wolfgang},
editor={Ermolayev, Vadim and Mayr, Heinrich C. and Nikitchenko, Mykola and Spivakovsky, Aleksander and Zholtkevych, Grygoriy},
title={Extending {F}loyd-{H}oare Logic for Partial Pre- and Postconditions},
bookTitle={Information and Communication Technologies in Education, Research, and Industrial Applications: 9th International
Conference, ICTERI 2013, Kherson, Ukraine, June 19--22, 2013, Revised Selected Papers},
year={2013},
publisher={Springer International Publishing},
pages={355--378},
isbn={978-3-319-03998-5},
doi={10.1007/978-3-319-03998-5_18},
url={https://doi.org/10.1007/978-3-319-03998-5_18}}

@article{NikitchKryvolap2013,
 author    = {Nikitchenko, Mykola and Kryvolap, Andrii},
 title     = {Properties of inference systems for {F}loyd-{H}oare Logic with partial predicates},
 journal   = {Acta Electrotechnica et Informatica},
 volume    = {13},
 number    = {4},
 pages     = {70--78},
 year      = {2013},
 doi={10.15546/aeei-2013-0052},
 url={https://doi.org/10.15546/aeei-2013-0052}}

@inproceedings{KornilowiczetalICTERI2017,
 author    = {Korni{\l}owicz, Artur and Kryvolap, Andrii and Nikitchenko, Mykola and Ivanov, Ievgen},
 title     = {An Approach To Formalization of an Extension of {F}loyd-{H}oare Logic},
 booktitle = {Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications.
Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, May 15--18, 2017},
 pages     = {504--523},
 year      = {2017},
 crossref  = {ICTERI2017},
 url       = {http://ceur-ws.org/Vol-1844/10000504.pdf}}

@proceedings{ICTERI2017,
 editor    = {Ermolayev, Vadim and Bassiliades, Nick and Fill, Hans-Georg and Yakovyna, Vitaliy and Mayr, Heinrich C. and
              Vyacheslav Kharchenko and Vladimir Peschanenko and Mariya Shyshkina and Mykola Nikitchenko and
              Spivakovsky, Aleksander},
 title     = {Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications.
Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, May 15--18, 2017},
 series    = {{CEUR} Workshop Proceedings},
 volume    = {1844},
 publisher = {CEUR-WS.org},
 year      = {2017},
 url       = {http://ceur-ws.org/Vol-1844}}

@inproceedings{DBLP:conf/fedcsis/KornilowiczKNI17,
 author    = {Kornilowicz, Artur and Kryvolap, Andrii and Nikitchenko, Mykola and Ivanov, Ievgen},
 title     = {Formalization of the Algebra of Nominative Data in {M}izar},
 booktitle = {Proceedings of the 2017 Federated Conference on Computer Science and
              Information Systems, FedCSIS 2017, Prague, Czech Republic, September
              3--6, 2017.},
 pages     = {237--244},
 year      = {2017},
 crossref  = {DBLP:conf/fedcsis/2017},
 url       = {https://doi.org/10.15439/2017F301},
 doi       = {10.15439/2017F301}}

@proceedings{DBLP:conf/fedcsis/2017,
 editor    = {Ganzha, Maria and Maciaszek, Leszek A. and Paprzycki, Marcin},
 title     = {Proceedings of the 2017 Federated Conference on Computer Science and
              Information Systems, FedCSIS 2017, Prague, Czech Republic, September
              3--6, 2017},
 year      = {2017},
 isbn      = {978-83-946253-7-5}}

@inproceedings{DBLP:conf/isat/KornilowiczKNI17,
 author    = {Kornilowicz, Artur and Kryvolap, Andrii and Nikitchenko, Mykola and Ivanov, Ievgen},
 title     = {Formalization of the Nominative Algorithmic Algebra in {M}izar},
 booktitle = {Information Systems Architecture and Technology: Proceedings of 38th
              International Conference on Information Systems Architecture and Technology
              -- {ISAT} 2017 -- Part II, Szklarska Por{\k{e}}ba, Poland, September
              17--19, 2017},
 pages     = {176--186},
 year      = {2017},
 crossref  = {DBLP:conf/isat/2017-2},
 url       = {https://doi.org/10.1007/978-3-319-67229-8_16},
 doi       = {10.1007/978-3-319-67229-8_16}}

@proceedings{DBLP:conf/isat/2017-2,
 editor    = {Borzemski, Leszek and {\'{S}}wi{\k{a}}tek, Jerzy and Wilimowska, Zofia},
 title     = {Information Systems Architecture and Technology: {P}roceedings of 38th
              International Conference on Information Systems Architecture and Technology
              -- {ISAT} 2017 -- {P}art {II}, {S}zklarska {P}or{\k{e}}ba, {P}oland, September
              17--19, 2017},
 series    = {Advances in Intelligent Systems and Computing},
 volume    = {656},
 publisher = {Springer},
 year      = {2018},
 url       = {https://doi.org/10.1007/978-3-319-67229-8},
 doi       = {10.1007/978-3-319-67229-8},
 isbn      = {978-3-319-67228-1}}

@inproceedings{Ivanov2014,
 author    = {Ivanov, Ievgen},
 title     = {On Representations of Abstract Systems with Partial Inputs and Outputs},
 booktitle = {Theory and Applications of Models of Computation -- 11th Annual Conference,
              {TAMC} 2014, Chennai, India, April 11--13, 2014. Proceedings},
 pages     = {104--123},
 year      = {2014},
 crossref  = {DBLP:conf/tamc/2014},
 url       = {https://doi.org/10.1007/978-3-319-06089-7_8},
 doi       = {10.1007/978-3-319-06089-7_8}}

@proceedings{DBLP:conf/tamc/2014,
 editor    = {Gopal, T. V. and Agrawal, Manindra and Li, Angsheng and Cooper, S. Barry},
 title     = {Theory and Applications of Models of Computation -- 11th Annual Conference,
              {TAMC} 2014, {C}hennai, {I}ndia, April 11--13, 2014. {P}roceedings},
 series    = {Lecture Notes in Computer Science},
 volume    = {8402},
 publisher = {Springer},
 year      = {2014},
 url       = {https://doi.org/10.1007/978-3-319-06089-7},
 doi       = {10.1007/978-3-319-06089-7},
 isbn      = {978-3-319-06088-0}}

@inproceedings{Ivanov2016,
 author    = {Ivanov, Ievgen},
 title     = {On Local Characterization of Global Timed Bisimulation for Abstract
              Continuous-Time Systems},
 booktitle = {Coalgebraic Methods in Computer Science -- 13th {IFIP} {WG} 1.3 {I}nternational
              Workshop, {CMCS} 2016, Colocated with {ETAPS} 2016, {E}indhoven, {T}he
              {N}etherlands, {A}pril 2--3, 2016, Revised Selected Papers},
 pages     = {216--234},
 year      = {2016},
 crossref  = {DBLP:conf/cmcs/2016},
 url       = {https://doi.org/10.1007/978-3-319-40370-0_13},
 doi       = {10.1007/978-3-319-40370-0_13}}

@proceedings{DBLP:conf/cmcs/2016,
 editor    = {Hasuo, Ichiro},
 title     = {Coalgebraic Methods in Computer Science -- 13th {IFIP} {WG} 1.3 International
              Workshop, {CMCS} 2016, Colocated with {ETAPS} 2016, {E}indhoven, {T}he
              {N}etherlands, April 2--3, 2016, Revised Selected Papers},
 series    = {Lecture Notes in Computer Science},
 volume    = {9608},
 publisher = {Springer},
 year      = {2016},
 url       = {https://doi.org/10.1007/978-3-319-40370-0},
 doi       = {10.1007/978-3-319-40370-0},
 isbn      = {978-3-319-40369-4}}

@inproceedings{DBLP:journals/corr/Ivanov17,
 author    = {Ivanov, Ievgen},
 title     = {On the Underapproximation of Reach Sets of Abstract Continuous-Time
              Systems},
 booktitle = {Proceedings 3rd International Workshop on Symbolic and Numerical Methods
              for Reachability Analysis, SNR@ETAPS 2017, Uppsala, Sweden, 22nd April
              2017},
 pages     = {46--51},
 year      = {2017},
 crossref  = {DBLP:journals/corr/AbrahamB17},
 url       = {https://doi.org/10.4204/EPTCS.247.4},
 doi       = {10.4204/EPTCS.247.4}}

@proceedings{DBLP:journals/corr/AbrahamB17,
 editor    = {{\'{A}}brah{\'{a}}m, Erika and Bogomolov, Sergiy},
 title     = {Proceedings 3rd International Workshop on Symbolic and Numerical Methods
              for Reachability Analysis, SNR@ETAPS 2017, Uppsala, Sweden, 22nd April
              2017},
 series    = {{EPTCS}},
 volume    = {247},
 year      = {2017},
 url       = {http://arxiv.org/abs/1704.02421}}

@proceedings{DBLP:conf/icteri/2014,
 editor = {Ermolayev, Vadim and Mayr, Heinrich C. and Nikitchenko, Mykola and Spivakovsky, Aleksander and Zholtkevych, Grygoriy},
 title     = {Information and Communication Technologies in Education, Research,
              and Industrial Applications -- 10th International Conference, {ICTERI}
              2014, {K}herson, {U}kraine, June 9--12, 2014, Revised Selected Papers},
 series    = {Communications in Computer and Information Science},
 volume    = {469},
 publisher = {Springer},
 year      = {2014},
 url       = {https://doi.org/10.1007/978-3-319-13206-8},
 doi       = {10.1007/978-3-319-13206-8},
 isbn      = {978-3-319-13205-1}}

@article{DBLP:journals/fm/IvanovNA15,
 author    = {Ivanov, Ievgen and Nikitchenko, Mykola and Abraham, Uri},
 title     = {Event-Based Proof of the Mutual Exclusion Property of {P}eterson's Algorithm},
 journal   = {Formalized Mathematics},
 volume    = {23},
 number    = {4},
 pages     = {325--331},
 year      = {2015},
 doi       = {10.1515/forma-2015-0026}}

@article{Nikitch2009,
 author    = {Nikitchenko, Mykola S.},
 title     = {Composition-nominative aspects of address programming},
 journal   = {Cybernetics and Systems Analysis},
 volume = {45},
 number = {864},
 year  = {2009},
 publisher = {Springer Science + Business Media, Inc.},
 note={(Translated from Kibernetika i~Sistemnyi Analiz, No. 6, pp. 24--35, November--December 2009)},
 doi = {10.1007/s10559-009-9159-4},
 url = {https://doi.org/10.1007/s10559-009-9159-4}}

@inproceedings{Nikitch2001,
author={Nikitchenko,  N.S.},
editor={Bjorner D., Broy M., Zamulin A.V.},
title={Abstract Computability of Non-deterministic Programs over Various Data Structures},
bookTitle={Perspectives of System Informatics: 4th International Andrei Ershov Memorial Conference, PSI 2001},
year={2001},
series={Lecture Notes in Computer Science},
volume={2244},
publisher={Springer, Berlin, Heidelberg},
pages={468--481},
doi={10.1007/3-540-45575-2_45},
url={https://doi.org/10.1007/3-540-45575-2_45}}

@incollection{grabowski2007revisions,
  title={Revisions as an essential tool to maintain mathematical repositories},
  author={Grabowski, Adam and Schwarzweller, Christoph},
  booktitle={Towards Mechanized Mathematical Assistants. Lecture Notes in Computer Science},
  editor = {Kauers, M. and Kerber, M. and Miner, R. and Windsteiger, W.},
  pages={235--249},
  volume = {4573},
  year={2007},
  publisher={Springer: Berlin, Heidelberg}}

@ARTICLE{harrison2007formalizing,
 TITLE={Formalizing basic complex analysis},
 AUTHOR={Harrison, John},
 JOURNAL={Studies in Logic, Grammar and Rhetoric},
 NUMBER={10},
 VOLUME={23},
pages={151--165},
 PUBLISHER={University of Bia{\l}ystok},
 YEAR={2007}}

@article{shidama2007formalization,
  title={On the formalization of {L}ebesgue integrals},
  author={Shidama, Yasunari and Endou, Noburu and Kawamoto, Pauline N.},
  journal={Studies in Logic, Grammar and Rhetoric},
  volume={10},
  number={23},
  pages={167--177},
 PUBLISHER={University of Bia{\l}ystok},
  year={2007}}

@article{boldo2016formalization,
  title={Formalization of real analysis: A survey of proof assistants and libraries},
  author={Boldo, Sylvie and Lelay, Catherine and Melquiond, Guillaume},
  journal={Mathematical Structures in Computer Science},
  volume={26},
  number={7},
  pages={1196--1233},
  year={2016},
  publisher={Cambridge University Press}}

@BOOK{HL99,
      AUTHOR = {L\"{u}neburg, Heinz},
      TITLE = {Gruppen, Ringe, K\"{o}rper: Die grundlegenden Strukturen der Algebra},
      PUBLISHER = {Oldenbourg Verlag},
      YEAR = {1990}}

@BOOK{Rad91alg1,
      AUTHOR = {Radbruch, Knut},
      TITLE = {Algebra {I}},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}

@ARTICLE{metamath,
author = {Megill, Norman D.},
title = {Metamath: {A} {C}omputer {L}anguage for {P}ure {M}athematics},
year = {2007},
publisher = {Lulu Press},
note = {\url{http://us.metamath.org/downloads/metamath.pdf}}}

@ARTICLE{HOL,
AUTHOR = {Harrison, John},
TITLE = {The {HOL} {L}ight System {REFERENCE}},
YEAR= {2014},
NOTE = {\url{http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf}}}

@ARTICLE{Matiyasevich,
  AUTHOR =       {Matiyasevich, Yuri},
  TITLE =        {Martin {D}avis and {H}ilbert's {T}enth {P}roblem},
  JOURNAL =      {Martin Davis on Computability, Computational Logic and Mathematical Foundations},
  YEAR =         {2017},
  pages =        {35--54}}


@ARTICLE{Lenstra,
  AUTHOR =       {Lenstra, Hendrik W.},
  TITLE =        {Solving the {P}ell equation},
  JOURNAL =      {Algorithmic Number Theory},
  YEAR =         {2008},
  volume =       {44},
  pages =        {1--24}}


@ARTICLE{Lagrange,
  AUTHOR =       {Lagrange, Joseph L.},
  TITLE =        {Solution d'un proble$\grave{e}$me d'arithm$\acute{e}$tique},
  JOURNAL =      {M$\acute{e}$langes de philosophie et de math. de la Soci$\acute{e}$t$\acute{e}$ Royale de Turin},
  YEAR =         {1773},
  number =       {44--97}}


@ARTICLE{KrumbiegelAmthor,
  AUTHOR =       {Krumbiegel, B. and Amthor, A.},
  TITLE =        {Das {P}roblema {B}ovinum des {A}rchimedes},
  JOURNAL =      {Historisch-literarische Abteilung der Zeitschrift fur Mathematik und Physik},
  YEAR =         {1880},
  volume =       {25},
  pages =        {121--136, 153--171}}

@MISC{MML1305,
    title = {{M}izar {M}athematical {L}ibrary, version: 5.44.1305},
    note = {\url{http://ftp.mizar.org/i386-win32/}},
howpublished = {Association of Mizar Users},
    year = {2017}}

@Inbook{Grabowski2018,
author={Grabowski, Adam and Mitsuishi, Takashi},
editor={Kacprzyk, Janusz
and Szmidt, Eulalia
and Zadro{\.{z}}ny, Slawomir
and Atanassov, K. T.
and Krawczak, Maciej},
title={Extending Formal Fuzzy Sets with Triangular Norms and Conorms},
bookTitle={Advances in Fuzzy Logic and Technology 2017: Proceedings of EUSFLAT'2017 and IWIFSGN'2017, Warsaw, Poland, Volume 2},
bookseries={Advances in Intelligent Systems and Computing},
volume={642: {\em Advances in Intelligent Systems and Computing}},
year={2018},
publisher={Springer International Publishing},
address={Cham},
pages={176--187},
doi={10.1007/978-3-319-66824-6_16},
url={https://doi.org/10.1007/978-3-319-66824-6_16}
}

@book{Baczynski:2008,
 author = {Baczy{\'n}ski, Micha{\l} and Jayaram, Balasubramaniam},
 title = {Fuzzy Implications},
 year = {2008},
 DOI = {10.1007/978-3-540-69082-5},
 publisher = {Springer Publishing Company, Incorporated}}
  
@ARTICLE{GrabowskiLTRS,
AUTHOR={Grabowski, Adam},
TITLE = {Lattice theory for rough sets -- a case study with {M}izar},
JOURNAL = {Fundamenta Informaticae},
VOLUME = {147},
NUMBER = {2--3}, 
PAGES = {223--240},
DOI = {10.3233/FI-2016-1406},
YEAR = 2016}

@BOOK{Schwartz1997a,
  TITLE={Th\'{e}orie des ensembles et topologie, tome 1. {A}nalyse},
  AUTHOR={Schwartz, Laurent},
  PUBLISHER={Hermann},
  YEAR={1997}}

@BOOK{Schwartz1997b,
  TITLE = {Calcul diff\'{e}rentiel, tome 2. {A}nalyse},
  AUTHOR = {Schwartz, Laurent},
  PUBLISHER = {Hermann},
  YEAR = {1997}}

@BOOK{driver2003,
  TITLE = {Analysis Tools with Applications},
  AUTHOR = {Driver, Bruce K.},
  PUBLISHER = {Springer, Berlin},
  YEAR = {2003}}

@BOOK{NIVEN:2008,
 AUTHOR={Niven, Ivan},
 TITLE={Diophantine Approximation},
 PUBLISHER={Dover},
 YEAR={2008}}

@ARTICLE{HURWITZ:1891,
 AUTHOR={Hurwitz, Adolf},
 TITLE={Ueber die angen{\"a}herte {D}arstellung der {I}rrationalzahlen durch rationale {B}r{\"u}che},
 JOURNAL={Mathematische Annalen},
 VOLUME={39},
 NUMBER={2},
 PAGES={279--284},
 URL = {https://eudml.org/doc/157573},
 YEAR={B.G.Teubner Verlag, Leipzig, 1891}}

@book{AdamowiczZbierski,
  author    = {Adamowicz, Zofia and Zbierski, Pawe{\l}},
  title     = {Logic of Mathematics: A Modern Course of Classical Logic},
  series    = {Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts},
  year      = {1997},
  publisher = {Wiley-Interscience}}

@ARTICLE{Hilbert10,
  AUTHOR =       {Davis, Martin},
  TITLE =        {Hilbert's Tenth Problem is Unsolvable},
  JOURNAL =      {The American Mathematical Monthly, Mathematical Association of America},
  YEAR =         {1973},
  volume =       {80},
  number =       {3},
  pages =        {233--269},
  DOI   =        {10.2307/2318447}}

@BOOK{MINKOWSKI:1907,
 AUTHOR={Minkowski, Hermann},
 TITLE={Diophantische {A}pproximationen: eine {E}inf{\"u}hrung in die {Z}ahlentheorie},
 PUBLISHER={Teubner, Leipzig},
 YEAR=1907}

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

@article{dhurdjevic2015automated,
title={Automated generation of machine verifiable and readable proofs: a case study of {T}arski's geometry},
author={Durdevic, Sana Stojanovic and Narboux, Julien and Jani{\v{c}}i{\'c}, Predrag},
journal={Annals of Mathematics and Artificial Intelligence},
volume={74},
number={3-4},
pages={249--269},
year= {2015},
publisher={Springer}}

@inproceedings{beeson2014otter,
title={{OTTER} proofs in {T}arskian geometry},
author={Beeson, Michael and Wos, Larry},
booktitle={International Joint Conference on Automated Reasoning},
pages={495--510},
year= {2014},
volume = {8562},
series = {Lecture Notes in Computer Science},
doi = {10.1007/978-3-319-08587-6_38},
publisher={Springer}}

@article{makarios:2014,
author={Makarios, Timothy James McKenzie},
title = {A further simplification of {T}arski's axioms of geometry},
journal={Note di Matematica},
volume={33},
number={2},
pages={123--132},
year={2014}}

@inproceedings{Grabowski:FedCSIS2016,
Author = {Grabowski, Adam},
Editor = {Ganzha, Maria and Maciaszek, Leszek and Paprzycki, Marcin},
Title = {{T}arski's Geometry Modelled in {M}izar Computerized Proof Assistant},
Booktitle = {Proceedings of the 2016 Federated Conference on Computer Science and
   Information Systems (FedCSIS)},
Series = {ACSIS -- Annals of Computer Science and Information Systems},
Year = {2016},
Volume = {8},
Pages = {373--381},
DOI = {10.15439/2016F290}
}

@book{Gupta:1965,
  author={Gupta, Haragauri Narayan},
  publisher={PhD thesis, University of California-Berkeley},
  year={1965},
  title={Contributions to the Axiomatic Foundations of Geometry}}

@article{Braun:2017,
  TITLE = {A synthetic proof of {P}appus' theorem in {T}arski's geometry},
  AUTHOR = {Braun, Gabriel and Narboux, Julien},
  URL = {https://hal.inria.fr/hal-01176508},
  JOURNAL = {{Journal of Automated Reasoning}},
  PUBLISHER = {{Springer Verlag}},
  VOLUME = {58},
  NUMBER = {2},
  PAGES = {23},
  YEAR = {2017},
  DOI = {10.1007/s10817-016-9374-4},
}