@article{HoldenKorovin:2025,
Author = {Holden, Edvard K. and Korovin, Konstantin},
Title = {Graph sequence learning for premise selection},
Journal = {Journal of Symbolic Computation},
Year = {2025},
Volume = {128},
Month = {May-Jun},
DOI = {10.1016/j.jsc.2024.102376},
Article-Number = {102376},
ISSN = {0747-7171},
EISSN = {1095-855X},
Unique-ID = {WOS:001312292300001}}

@inproceedings{ WOS:001292779800018,
Author = {Jakubuv, Jan and Janota, Mikolas and Urban, Josef},
Editor = {Kohlhase, A. and Kovacs, L.},
Title = {Solving Hard {M}izar Problems with Instantiation and Strategy Invention},
Booktitle = {Intelligent Computer Mathematics, {CICM} 2024},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2024},
Volume = {14690},
Pages = {315--333},
Note = {17th International Conference on Intelligent Computer Mathematics (CICM), Montreal, Canada, Aug. 05--09, 2024},
DOI = {10.1007/978-3-031-66997-2\_18},
ISSN = {2945-9133},
EISSN = {1611-3349},
ISBN = {978-3-031-66996-5; 978-3-031-66997-2},
Unique-ID = {WOS:001292779800018}}

@inproceedings{KaiNakasho:2024,
Author = {Kai, Toshiki and Teruya, Yuta and Nakasho, Kazuhisa},
Editor = {Kohlhase, A. and Kovacs, L.},
Title = {Remote Verification System for {M}izar Integrated with {E}mwiki},
Booktitle = {Intelligent Computer Mathematics, {CICM} 2024},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2024},
Volume = {14690},
Pages = {337--344},
Note = {17th International Conference on Intelligent Computer Mathematics (CICM), Montreal, Canada, Aug. 05-09, 2024},
DOI = {10.1007/978-3-031-66997-2\_19},
ISSN = {2945-9133},
EISSN = {1611-3349},
ISBN = {978-3-031-66996-5; 978-3-031-66997-2},
Unique-ID = {WOS:001292779800019}}

@article{TomaszukSzeremeta:2023,
Author = {Tomaszuk, Dominik and Szeremeta, {\L}ukasz and Korni{\l}owicz, Artur},
Title = {{MMLKG}: Knowledge Graph for Mathematical Definitions, Statements and Proofs},
Journal = {Scientific Data},
Year = {2023},
Volume = {10},
Number = {1},
DOI = {10.1038/s41597-023-02681-3},
Article-Number = {791},
EISSN = {2052-4463},
Unique-ID = {WOS:001103408600004}}

@article{KaliszykPak:2023,
Author = {Kaliszyk, Cezary and P\k{a}k, Karol},
Title = {Combining Higher-Order Logic with Set Theory Formalizations},
Journal = {Journal of Automated Reasoning},
Year = {2023},
Volume = {67},
Number = {2},
Month = {JUN},
DOI = {10.1007/s10817-023-09663-5},
Article-Number = {20},
ISSN = {0168-7433},
EISSN = {1573-0670},
Unique-ID = {WOS:000994243900001}}

@inproceedings{JakubuvKaliszyk:2023,
Author = {Jakubuv, Jan and Kaliszyk, Cezary},
Editor = {Dubois, C. and Kerber, M.},
Title = {{V}iz{AR}: Visualization of Automated Reasoning Proofs (System Description)},
Booktitle = {Intelligent Computer Mathematics, {CICM} 2023},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2023},
Volume = {14101},
Pages = {303--308},
Note = {16th International Conference on Intelligent Computer Mathematics (CICM), Cambridge, England, Sep. 05--08, 2023},
DOI = {10.1007/978-3-031-42753-4\_22},
ISSN = {2945-9133},
EISSN = {1611-3349},
ISBN = {978-3-031-42752-7; 978-3-031-42753-4},
Unique-ID = {WOS:001292771100022}}

@inproceedings{Naumowicz:2023,
Author = {Naumowicz, Adam},
Editor = {Dubois, C. and Kerber, M.},
Title = {Extending Numeric Automation for Number Theory Formalizations in {M}izar},
Booktitle = {Intelligent Computer Matheatics, {CICM} 2023},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2023},
Volume = {14101},
Pages = {309--314},
Note = {16th International Conference on Intelligent Computer Mathematics (CICM), Cambridge, ENGLAND, SEP 05-08, 2023},
DOI = {10.1007/978-3-031-42753-4\_23},
ISSN = {2945-9133},
EISSN = {1611-3349},
ISBN = {978-3-031-42752-7; 978-3-031-42753-4},
ResearcherID-Numbers = {Naumowicz, Adam/L-6183-2018},
Unique-ID = {WOS:001292771100023}}


@inproceedings{GrabowskiFUZZ:2023,
Author = {Grabowski, Adam},
Book-Group-Author = {IEEE},
Title = {Computer-Supported Encoding of Fuzzy Negations and Laws of Contraposition},
Booktitle = {2023 {IEEE} International Conference of Fuzzy Systems, {FUZZ-IEEE}},
Series = {IEEE International Fuzzy Systems Conference Proceedings},
Year = {2023},
Note = {IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), Incheon, South Korea, Aug. 13--17, 2023},
DOI = {10.1109/FUZZ52849.2023.10309683},
ISSN = {1544-5615},
ISBN = {979-8-3503-3228-5},
Unique-ID = {WOS:001103277400015}}

@article{ WOS:000899419900046,
Author = {Abdelaziz, Ibrahim and Crouse, Maxwell and Makni, Bassem and Austel,
   Vernon and Cornelio, Cristina and Ikbal, Shajith and Kapanipathi, Pavan
   and Makondo, Ndivhuwo and Srinivas, Kavitha and Witbrock, Michael and
   Fokoue, Achille},
Title = {Learning to Guide a Saturation-Based Theorem Prover},
Journal = {IEEE TRANSACTIONS ON PATTERN ANALYSIS AND MACHINE INTELLIGENCE},
Year = {2023},
Volume = {45},
Number = {1},
Pages = {738--751},
Month = {JAN 1},
DOI = {10.1109/TPAMI.2022.3140382},
ISSN = {0162-8828},
EISSN = {1939-3539},
ResearcherID-Numbers = {Abdelaziz, Ibrahim/AAE-2152-2021
   Witbrock, Michael/KUC-6680-2024
   },
ORCID-Numbers = {Makondo, Ndivhuwo/0000-0002-4147-3328
   Crouse, Maxwell/0000-0002-7327-7508},
Unique-ID = {WOS:000899419900046}}

%%==========================================================================================================

@inproceedings{FurushimaYamamichi:2022,
Author = {Furushima, Hideharu and Yamamichi, Daichi and Shigenaka, Seigo and
   Nakasho, Kazuhisa and Wasaki, Katsumi},
Editor = {Buzzard, K. and Kutsia, T.},
Title = {An Integrated Web Platform for the {M}izar {M}athematical {L}ibrary},
Booktitle = {Intelligent Computer Mathematics, {CICM} 2022},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2022},
Volume = {13467},
Pages = {141--146},
Note = {15th International Conference on Intelligent Computer Mathematics (CICM), part of the Computational Logic Autumn Summit (CLAS), Ivane
   Javakhishvili Tbilisi State Univ, Tbilisi, Georgia, Sep. 19--30, 2022},
DOI = {10.1007/978-3-031-16681-5\_9},
ISSN = {0302-9743},
EISSN = {1611-3349},
ISBN = {978-3-031-16681-5; 978-3-031-16680-8},
Unique-ID = {WOS:000870055900009}}

@article{KohlhaseRabe:2021,
Author = {Kohlhase, Michael and Rabe, Florian},
Title = {Experiences from Exporting Major Proof Assistant Libraries},
Journal = {Journal of Automated Reasoning},
Year = {2021},
Volume = {65},
Number = {8},
Pages = {1265--1298},
DOI = {10.1007/s10817-021-09604-0},
ISSN = {0168-7433},
EISSN = {1573-0670},
Unique-ID = {WOS:000680802300002}}

@article{PurgalParsert:2021,
Author = {Purgal, Stanis{\l}aw and Parsert, Julian and Kaliszyk, Cezary},
Title = {A study of continuous vector representations for theorem proving},
Journal = {Journal of Logic and Computation},
Year = {2021},
Volume = {31},
Number = {8},
Pages = {2057--2083},
Month = {DEC},
DOI = {10.1093/logcom/exab006},
EarlyAccessDate = {FEB 2021},
ISSN = {0955-792X},
EISSN = {1465-363X},
Unique-ID = {WOS:000744734200008}}

@inproceedings{ WOS:000802219100025,
Author = {Taniguchi, Hirota and Nakasho, Kazuhisa},
Book-Group-Author = {IEEE},
Title = {Visual Studio Code Extension and Auto-completion for {M}izar Language},
Booktitle = {2021 NINTH INTERNATIONAL SYMPOSIUM ON COMPUTING AND NETWORKING (CANDAR 2021)},
Series = {International Symposium on Computing and Networking},
Year = {2021},
Pages = {182--188},
Note = {9th International Symposium on Computing and Networking (CANDAR), ELECTR NETWORK, NOV 23-26, 2021},
DOI = {10.1109/CANDAR53791.2021.00033},
ISSN = {2379-1888},
ISBN = {978-1-6654-4246-6},
ResearcherID-Numbers = {Nakasho, Kazuhisa/W-8584-2019},
Unique-ID = {WOS:000802219100025}}

@inproceedings{GoertzelChvalovsky:2021,
Author = {Goertzel, Zarathustra A. and Chvalovsky, Karel and Jakubuv, Jan and
   Olsak, Miroslav and Urban, Josef},
Editor = {Konev, B. and Reger, G.},
Title = {Fast and Slow Enigmas and Parental Guidance},
Booktitle = {FRONTIERS OF COMBINING SYSTEMS (FROCOS 2021)},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2021},
Volume = {12941},
Pages = {173--191},
Note = {13th International Symposium on Frontiers of Combining Systems (FroCoS),
   Birmingham Univ, Birmingham, ENGLAND, SEP 08-10, 2021},
Organization = {Springer},
DOI = {10.1007/978-3-030-86205-3\_10},
ISSN = {0302-9743},
EISSN = {1611-3349},
ISBN = {978-3-030-86205-3; 978-3-030-86204-6},
Unique-ID = {WOS:000711401800010}}

@inproceedings{ WOS:000711401800011,
Author = {Suda, Martin},
Editor = {Konev, B. and Reger, G.},
Title = {Vampire with a Brain Is a Good {ITP} Hammer},
Booktitle = {FRONTIERS OF COMBINING SYSTEMS (FROCOS 2021)},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2021},
Volume = {12941},
Pages = {192--209},
Note = {13th International Symposium on Frontiers of Combining Systems (FroCoS),
   Birmingham Univ, Birmingham, ENGLAND, SEP 08-10, 2021},
Organization = {Springer},
DOI = {10.1007/978-3-030-86205-3\_11},
ISSN = {0302-9743},
EISSN = {1611-3349},
ISBN = {978-3-030-86205-3; 978-3-030-86204-6},
Unique-ID = {WOS:000711401800011}}

@inproceedings{ WOS:000707054900017,
Author = {Rothgang, Colin and Korni{\l}owicz, Artur and Rabe, Florian},
Editor = {Kamareddine, F. and Coen, C.S.},
Title = {A New Export of the {M}izar {M}athematical {L}ibrary},
Booktitle = {INTELLIGENT COMPUTER MATHEMATICS (CICM 2021)},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2021},
Volume = {12833},
Pages = {205-210},
Note = {14th International Conference on Intelligent Computer Mathematics
   (CICM), ELECTR NETWORK, JUL 26-31, 2021},
DOI = {10.1007/978-3-030-81097-9\_17},
ISSN = {0302-9743},
EISSN = {1611-3349},
ISBN = {978-3-030-81097-9; 978-3-030-81096-2},
Unique-ID = {WOS:000707054900017}}

@inproceedings{CrouseAbdelaziz:2021,
Author = {Crouse, Maxwell and Abdelaziz, Ibrahim and Makni, Bassem and Whitehead,
   Spencer and Cornelio, Cristina and Kapanipathi, Pavan and Srinivas,
   Kavitha and Thost, Veronika and Witbrock, Michael and Fokoue, Achille},
Book-Group-Author = {Assoc Advancement Artificial Intelligence},
Title = {A Deep Reinforcement Learning Approach to First-Order Logic Theorem
   Proving},
Booktitle = {Thirt-Fifth AAAI Conference on Artificial Intelligence, Thirty-Third
   Conference on Innovative Applications of Artificial Intelligence and the 
   Eleventh Symposium on Educational Advances in Artificial Intelligence},
Series = {AAAI Conference on Artificial Intelligence},
Year = {2021},
Volume = {35},
Pages = {6279--6287},
Note = {35th AAAI Conference on Artificial Intelligence / 33rd Conference on
   Innovative Applications of Artificial Intelligence / 11th Symposium on
   Educational Advances in Artificial Intelligence, ELECTR NETWORK, Feb.
   02--09, 2021},
Organization = {Assoc Advancement Artificial Intelligence},
ISSN = {2159-5399},
EISSN = {2374-3468},
ISBN = {978-1-57735-866-4},
Unique-ID = {WOS:000680423506044}}

@article{WOS:000629178200005,
Author = {Grabowski, Adam},
Title = {Automated Comparative Study of Some Generalized Rough Approximations},
Journal = {Fundamenta Informaticae},
Year = {2021},
Volume = {179},
Number = {2},
Pages = {165-182},
DOI = {10.3233/FI-2021-2019},
ISSN = {0169-2968},
EISSN = {1875-8681},
Unique-ID = {WOS:000629178200005}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@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\k{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},
         YEAR = {1982}}

@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, Alexander},
        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{\"a}tzer, 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, Martin and Ziegler, G{\"u}nter 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{\"a}hlter 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={Yosida, K{\^o}saku},
 TITLE={Functional Analysis},
 PUBLISHER={Springer},
 YEAR={1980}}

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

@BOOK{Dunford:1958,
 AUTHOR={Dunford, Nelson and Schwartz, Jacob 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{\"u}nbaum, 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{ThomasJech2003,
       AUTHOR = {Jech, Thomas},
        TITLE = {Set Theory},
    PUBLISHER = {Springer-Verlag},
         YEAR = {2003},
          DOI = {10.1007/3-540-44761-X},
          URL = {http://dx.doi.org/10.1007/3-540-44761-X},
      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/},
    NOTE = {Available online at {\tt http://www.cs.ru.nl/\~{}freek/100/}}}

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

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

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

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

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

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

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

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

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

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

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

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

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

@article{Pawlak1982,
  author    = {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, John Horton},
     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{\"o}ger, 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{\"u}hrung
  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},
 VOLUME={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 University Press},
  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, Heinz-Dieter and Flum, J{\"o}rg and Thomas, Wolfgang},
  year={1994},
  publisher={Springer}}

@article{caminati2009yet,
  title={Yet another proof of {G}oedel'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{\"o}llmer, 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{\"u}hrung in die Mathematische Logik},
 YEAR = {2007},
 PUBLISHER = {Springer-Verlag, Berlin Heidelberg}}

@BOOK{Goedel:1930,
 AUTHOR={G{\"o}del, Kurt},
 TITLE={Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls},
 PUBLISHER={Monatshefte f{\"u}r 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, K{\^o}saku},
 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{\"a}user},
   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{\'e}n, S{\"o}ren},
 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{\"a}tzer, George},
 TITLE={Lattice Theory: Foundation},
 YEAR=2011,
 PUBLISHER = {Birkh{\"a}user}}

@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{\"a}user, 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},
DOI = {10.1016/S0019-9958(65)90241-X}}

@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, Joseph J.},
  TITLE     = {An Introduction to the Theory of Groups},
  PUBLISHER = {Springer},
  YEAR      = {1995}}

@book{robinson2012course,
  AUTHOR    = {Robinson, Derek},
  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 Horton},
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, Edward 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{\"a}rvinen, 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{\"a}tzer, 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, Vladimir Igorevich},
  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},
doi = {10.1007/978-3-642-30958-8}}

@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},
   NOTE = {\href{http://mediatum.ub.tum.de/node?id=1175107}{\tt http://mediatum.ub.tum.de/node?id=1175107}},
  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},
   NOTE = {\href{https://pl.scribd.com/doc/180234043/Knopp-Infinite-Sequences-and-Series-1956-pdf}{\tt https://pl.scribd.com/doc/180234043/Knopp-Infinite-Sequences-and-Series-1956-pdf}},
  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, Walter Warwick},
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},
  series = {Translations of Mathematical Monographs},
  volume = {125},
  year={1985},
  publisher={American Mathematical Society}}

@book{matsumura1989,
  title={Commutative Ring Theory},
  author={Matsumura, Hideyuki},
  series ={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, John Horton 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},
  PUBLISHER = {Cambridge Univ. Press},
  YEAR = {2013},
  ISBN = {978-1-107-00548-8},
  DOI = {10.1017/CBO9780511794216},
  PAGES = {XXVI, 979 S.},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?32611138_toc.pdf}{\tt http://scans.hebis.de/HEBCGI/show.pl?32611138_toc.pdf}},
  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.},
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},
  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}}

@Inproceedings{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    = {Korni{\l}owicz, 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    = {Korni{\l}owicz, 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 = {1999}}

@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},
 PUBLISHER = {B.G.Teubner Verlag, Leipzig},
 YEAR = {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}}

@book{heinz:2002,
author={Bauer, Heinz},
title={Wahrscheinlichkeitstheorie},
publisher={de Gruyter-Verlag},
year={2002},
ADDRESS={Berlin, New York}}


@book{Kleene1952,
  title={Introduction to Metamathematics},
  author={Kleene, S.C.},
  year={1952},
  publisher={North-Holland Publishing Co., Amsterdam, and P. Noordhoff, Groningen}}


@book{Brignole1964,
author={Brignole, Diana and Monteiro, Antonio},
title={Caract\'erisation des alg\`ebres de {N}elson par des egalit\'es},
year={1964},
publisher={Instituto de Matem\'atica, Universidad Nacional del Sur, Argentina}}


@article{Kalman1958,
        doi = {10.1090/s0002-9947-1958-0095135-x},
        year = 1958,
        month = {February},
        publisher = {American Mathematical Society ({AMS})},
        volume = {87},
        number = {2},
        pages = {485--485},
        author = {Kalman, J. A.},
        title = {Lattices with involution},
        journal = {Transactions of the American Mathematical Society}}


@article{Monteiro1996,
        year = 1996,
        publisher = {Unpublished Papers, Instituto de Matem\'atica -- Universidad Nacional del Sur -- 1973, Bah\'ıa Blanca -- Argentina},
        number = {40},
        pages = {1--11},
        author = {Monteiro, Antonio and Monteiro, Luiz},
        title = {Axiomes ind\'ependants pour les alg\`ebres de {N}elson, de {{\L}}ukasiewicz trivalentes, de De {M}organ et de {K}leene},
        journal = {Notas de l\'ogica matem\'atica}}


@article{Cignoli1975,
 author = {Cignoli, Roberto},
 journal = {Proceedings of the American Mathematical Society},
 number = {2},
 pages = {269--278},
 publisher = {American Mathematical Society},
 title = {Injective de {M}organ and {K}leene Algebras},
 volume = {47},
 year = {1975}}

@book{Blyth1994,
  title={Ockham Algebras},
  author={Blyth, T.S. and Varlet, J.},
  series={Oxford science publications},
  year={1994},
  publisher={Oxford University Press}}

@Inbook{Kozen1990,
author={Kozen, Dexter},
editor={Rovan, Branislav},
title={On {K}leene algebras and closed semirings},
bookTitle={Mathematical Foundations of Computer Science 1990: Bansk{\'a} Bystrica, Czechoslovakia August 27--31, 1990 Proceedings},
year={1990},
publisher={Springer Berlin Heidelberg},
pages={26--47},
doi={10.1007/BFb0029594}}

@book{Conway1971,
  title={Regular algebra and finite machines},
  author={Conway, John Horton},
  series={Chapman and Hall mathematics series},
  year={1971},
  publisher={Chapman and Hall}}

@book{Cleave1991,
  title={A~Study of Logics},
  author={Cleave, J.P.},
  isbn={9780198532118},
  series={Oxford logic guides},
  year={1991},
  publisher={Clarendon Press}}


@book{Korner1966,
  title={Experience and Theory: An Essay in the Philosophy of Science},
  author={K{\"o}rner, S.},
  series={International library of philosophy and scientific method},
  year={1966},
  publisher={Routledge \& Kegan Paul}}


@article{NikShk2017:QE-calculus,
  author    = {Nikitchenko, Mykola and Shkilniak, Stepan},
  title = {Algebras and Logics of Partial Quasiary Predicates},
 journal   = {Algebra and Discrete Mathematics},
  volume    = {23},
  number    = {2},
  year      = {2017},
  pages     = {263--278}}


@article{Negri1998,
    AUTHOR = {Negri, Maurizio},
     TITLE = {{DMF}-algebras: representation and topological characterization},
   JOURNAL = {Boll. Unione Mat. Ital. Sez. B Artic. Ric. Mat. (8)},
  FJOURNAL = {Bollettino della Unione Matematica Italiana. Serie {VIII}.
              Sezione B. Articoli di Ricerca Matematica},
    VOLUME = {1},
      YEAR = {1998},
    NUMBER = {2},
     PAGES = {369--390}}


@article{Negri1996,
    AUTHOR = {Negri, Maurizio},
     TITLE = {Three valued semantics and {DMF}-algebras},
   JOURNAL = {Boll. Un. Mat. Ital. B (7)},
  FJOURNAL = {Unione Matematica Italiana. Bollettino. B. Serie {VII}},
    VOLUME = {10},
      YEAR = {1996},
    NUMBER = {3},
     PAGES = {733--760}}

@misc{Negri2013,
Author = {Negri, Maurizio},
Title = {Partial Probability and {K}leene Logic},
Year = {2013},
Eprint = {arXiv:1310.6172}}


@Inproceedings{Kornilowicz2018,
author={Korni{\l}owicz, Artur and Kryvolap, Andrii and Nikitchenko, Mykola and Ivanov, Ievgen},
editor={{\'{S}}wi{\k{a}}tek, Jerzy and Borzemski, Leszek and Wilimowska, Zofia},
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}},
year={2018},
publisher={Springer International Publishing},
pages={176--186},
isbn={978-3-319-67229-8},
doi={10.1007/978-3-319-67229-8_16},
url={https://doi.org/10.1007/978-3-319-67229-8_16}}


@Inproceedings{Ivanov2014a,
author={Ivanov, Ievgen and Nikitchenko, Mykola and Abraham, Uri},
editor={Ermolayev, Vadim and Mayr, Heinrich C. and Nikitchenko, Mykola and Spivakovsky, Aleksander and Zholtkevych, Grygoriy},
title={On a Decidable Formal Theory for Abstract Continuous-Time Dynamical Systems},
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},
year={2014},
publisher={Springer International Publishing},
pages={78--99},
isbn={978-3-319-13206-8},
doi={10.1007/978-3-319-13206-8_4},
url={https://doi.org/10.1007/978-3-319-13206-8_4}}


@article{beltrami1868saggio,
  title={Saggio di interpetrazione della geometria non-euclidea},
  author={Beltrami, Eugenio},
  journal={Giornale di Matematiche},
  volume={6},
  pages={284--322},
  year={1868}}


@inproceedings{beltrami1869essai,
  title={Essai d'interpr{\'e}tation de la g{\'e}om{\'e}trie non-euclid{\'e}enne},
  author={Beltrami, Eugenio},
  booktitle={Annales scientifiques de l'{\'E}cole {N}ormale {S}up{\'e}rieure. {T}rad. par J. Ho{\"u}el},
  volume={6},
  pages={251--288},
  year={1869},
  organization={Elsevier}}

@book{BS55,
  title={Podstawy geometrii},
  author={Borsuk, Karol and Szmielew, Wanda},
  year={1955 (in Polish)},
  publisher={Pa\'nstwowe {W}ydawnictwo {N}aukowe, {W}arszawa}}

@inproceedings{hoelzl2011measuretheory,
  author       = {H{\"o}lzl, Johannes and Heller, Armin},
  title        = {Three Chapters of Measure Theory in {Isabelle/HOL}},
  year         = {2011},
  pages        = {135--151},
  editor       = {van Eekelen, Marko C. J. D. and Geuvers, Herman and Schmaltz, Julien and Wiedijk, Freek},
  booktitle    = {Interactive Theorem Proving (ITP 2011)},
  series       = {LNCS},
  volume       = {6898}}

@article{a2014klein,
title = {On {K}lein's so-called non-{E}uclidean geometry},
author = {A'Campo, Norbert and Papadopoulos, Athanase},
journal = {arXiv preprint arXiv:1406.7309},
url = {https://arxiv.org/pdf/1406.7309.pdf},
year = {2014}}

@BOOK{LNT:Smorynski,
  AUTHOR =       {Smorynski, Craig Alan},
  TITLE =        {Logical Number Theory {I}, An Introduction},
  PUBLISHER =    {Springer-Verlag Berlin Heidelberg},
  YEAR =         {1991},
  series =       {Universitext},
  isbn =         {978-3-642-75462-3}}

@Article{BancerekJAR:2018,
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},
title={The Role of the {M}izar {M}athematical {L}ibrary for Interactive Proof Development in {M}izar},
journal={Journal of Automated Reasoning},
year={2018},
volume={61},
number={1},
pages={9--32},
doi={10.1007/s10817-017-9440-6},
url={https://doi.org/10.1007/s10817-017-9440-6}}

@ARTICLE{Euler:1737,
  AUTHOR =       {Euler, Leonhard},
  TITLE =        {Variae observationes circa series infinitas},
  JOURNAL =    {Commentarii Academiae Scientiarum Petropolitanae},
  YEAR =         {1737},
  VOLUME = {9},
   PAGES = {160--188}}

@book{SIMPLE,
  TITLE = {Introduction to Graph Theory},
  AUTHOR = {Wilson, Robin James},
  ADDRESS = {Edinburgh},
  PUBLISHER = {Oliver \& Boyd},
  YEAR = {1972},
  ISBN = {0-05-002534-1},
  PAGES = {VIII, 168},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf}{\tt http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf}},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf}}

@book{MULTI,
  TITLE = {Graph Theory},
  SERIES = {Graduate Texts in Mathematics, 244},
  AUTHOR = {Bondy, John Adrian and Murty, U. S. R.},
  ADDRESS = {New York},
  PUBLISHER = {Springer},
  YEAR = {2008},
  ISBN = {978-1-84628-969-9},
  PAGES = {XII, 652},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf}{\tt http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf}},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf}}

@book{SELECTED,
  TITLE = {Selected Topics in Graph Theory},
  EDITOR = {Beineke, Lowell W. and Wilson, Robin J.},
  ADDRESS = {London},
  PUBLISHER = {Academic Press},
  YEAR = {1978},
  ISBN = {0-12-086250-6},
  pages = {IX, 451}}

@article{Moldova2018,
         author    = {Ivanov, Ievgen and Korni{\l}owicz, Artur and Nikitchenko, Mykola},
         title     = {Implementation of the Composition-Nominative Approach to Program Formalization in {M}izar},
         journal   = {The Computer Science Journal of Moldova},
         volume    = {26},
         number    = {1},
         pages     = {59--76},
         year      = {2018},
         url       = {http://www.math.md/publications/csjm/issues/v26-n1/12569/}}

@inproceedings{SeqRule2018,
 author    = {Ivanov, Ievgen and Nikitchenko, Mykola},
 title     = {On the Sequence Rule for the {F}loyd-{H}oare Logic with Partial Pre- and Post-Conditions},
 booktitle = {Proceedings of the 14th International Conference on ICT in Education, Research and Industrial Applications.
Integration, Harmonization and Knowledge Transfer. Volume II: Workshops, Kyiv, Ukraine, May 14--17, 2018},
 series = {CEUR Workshop Proceedings},
 volume = {2104},
 pages     = {716--724},
 year      = {2018}}

@Article{Zazkis1998,
author={Zazkis, Rina},
title={Odds and Ends of Odds and Evens: An Inquiry Into Students' Understanding of Even and Odd Numbers},
journal={Educational Studies in Mathematics},
year={1998},
month={Jun},
day={01},
volume={36},
number={1},
pages={73--89},
issn={1573-0816},
doi={10.1023/A:1003149901409},
url={https://doi.org/10.1023/A:1003149901409}}

@book{sawyer2003vision,
  title={Vision in Elementary Mathematics},
  author={Sawyer, Walter Warwick},
  year={2003},
  publisher={Courier Corporation}}

@book{russo2013forgotten,
title={The forgotten revolution: how science was born in 300 {BC} and why it had to be reborn},
author={Russo, Lucio and Levy (translator), Silvio},
year={2013},
publisher={Springer Science \& Business Media}}

@article{Gomolinska2002,
  title={A comparative study of some generalized rough approximations},
  author={Gomoli\'nska, Anna},
  journal={Fundamenta Informaticae},
  volume={51},
  pages={103--119},
  year={2002}}

@book{German,
title = {Graphentheorie},
series = {B.I-Hochschultaschenb{\"u}cher; 248},
author = {Wagner, Klaus},
address = {Mannheim},
publisher = {Bibliograph. Inst.},
year = {1970},
ISBN = {3-411-00248-4},
pages = {220}}

@book{GERWAG,
title = {Graphentheorie},
series = {B.I-Hochschultaschenb{\"u}cher; 248},
author = {Wagner, Klaus},
address = {Mannheim},
publisher = {Bibliograph. Inst.},
year = {1970},
ISBN = {3-411-00248-4},
pages = {220}}

@book{Padma2008,
title={Axioms for Lattices and {B}oolean Algebras},
author={Padmanabhan, Ranganathan and Rudeanu, Sergiu},
year={2008},
publisher={World Scientific Publishers}}

@book{Padma1996,
title={Automated Deduction in Equational Logic and Cubic Curves},
author={McCune, William and Padmanabhan, Ranganathan},
year={1996},
publisher={Springer-Verlag, Berlin}}

@article{Sholander1951,
  title={Postulates for Distributive Lattices},
  author={Sholander, Marlow},
  journal={Canadian Journal of Mathematics},
  volume={3},
  pages={28--30},
  year={1951},
  doi={10.4153/CJM-1951-003-5}}

@article{McKenzie1970,
  title={Equational Bases for Lattice Theories},
  author={McKenzie, Ralph},
  journal={Mathematica Scandinavica},
  volume={27},
  pages={24--38},
  year={1970},
  doi={10.7146/math.scand.a-10984}}

@unpublished{prover9-mace4,
    author = {McCune, William},
    title = {Prover9 and {M}ACE4},
    url = {http://www.cs.unm.edu/~mccune/prover9/},
    year = {2005--2010}}

@inproceedings{EqualityFedCSIS,
Author = {Grabowski, Adam and Korni{\l}owicz, Artur and Schwarzweller, Christoph},
Editor = {{Ganzha, Maria and Maciaszek, Leszek and Paprzycki, Marcin}},
Title = {Equality in Computer Proof-Assistants},
Booktitle = {Proceedings of the 2015 Federated Conference on Computer Science and Information Systems},
Series = {ACSIS-Annals of Computer Science and Information Systems},
Year = {2015},
Volume = {5},
Pages = {45--54},
Publisher = {{IEEE}},
DOI = {10.15439/2015F229}}

@inproceedings{SchwarzRCA:2004,
Author = {Grabowski, Adam and Schwarzweller, Christoph},
Editor = {Asperti, Andrea and Bancerek, Grzegorz and Trybulec, Andrzej},
Title = {Rough {C}oncept {A}nalysis -- Theory development in the {M}izar system},
booktitle = {Mathematical Knowledge Management, Third International Conference,
               {MKM} 2004, Bialowieza, Poland, September 19--21, 2004, Proceedings},
Series = {Lecture Notes in Computer Science},
doi       = {10.1007/978-3-540-27818-4_10},
Year = {2004},
Volume = {3119},
Pages = {130--144},
Note = {3rd International Conference on Mathematical Knowledge Management,
   Bialowieza, Poland, Sep. 19-21, 2004}}

@Inproceedings{Naumowicz2009,
  author       = {Naumowicz, Adam and Korni{\l}owicz, Artur},
  title        = {A brief overview of {M}izar},
  booktitle    = {International Conference on Theorem Proving in Higher Order Logics},
  year         = {2009},
  pages        = {67--72},
  DOI = {10.1007/978-3-642-03359-9_5},
  publisher = {Springer}}

@InProceedings{Elizarov2017,
author={Elizarov, Alexander and Kirillovich, Alexander and Lipachev, Evgeny and Nevzorova, Olga},
editor={Kalinichenko, Leonid and Kuznetsov, Sergei O. and Manolopoulos, Yannis},
title={Digital Ecosystem {O}nto{M}ath: Mathematical Knowledge Analytics and Management},
booktitle={Data Analytics and Management in Data Intensive Domains},
year={2017},
publisher={Springer International Publishing},
pages={33--46}}

@InProceedings{Rudnicki2003,
  author        = {Rudnicki, Piotr and Trybulec, Andrzej},
  booktitle       = {Mathematical Knowledge Management},
  title         = {On the Integrity of a Repository of Formalized Mathematics},
  volume = {2594},
  series = {Lecture Notes in Computer Science},
  editor = {Asperti, Andrea and Buchberger, Bruno and Davenport, James H.},
  year          = {2003},
  pages = {162--174},
  doi           = {10.1007/3-540-36469-2_13},
  publisher     = {Springer, Berlin, Heidelberg}}


@BOOK{MUNKRES,
  TITLE = {Topology},
  AUTHOR = {Munkres, James Raymond},
  ADDRESS = {Upper Saddle River, NJ},
  PUBLISHER = {Prentice-Hall},
  YEAR = {2000},
  EDITION = {2},
  PAGES = {XVI, 537 pages}}


@phdthesis{baskevitch2008,
  title={Les repr{\'e}sentations de la propagation du son, d'{A}ristote {\`a} l'{E}ncyclop{\'e}die},
  author={Baskevitch, Fran{\c{c}}ois},
  year={2008},
  school={Universit{\'e} de Nantes, France}}


@book{parzysz1984musique,
  title={Musique et math{\'e}matique: (suivi de) {G}ammes naturelles},
  author={Parzysz, Bernard and Hellegouarch, Yves},
  year={1984},
  number={53},
  publisher={Association des Professeurs de Math\'ematiques de l'Enseignement Public (APMEP), Paris}}


@BOOK{IITAKA1982,
 AUTHOR={Iitaka, Shigeru},
 TITLE={Algebraic Geometry: An Introduction to Birational Geometry of Algebraic Varieties},
 PUBLISHER={Springer-Verlag New York, Inc.},
 YEAR={1982}}

@BOOK{IITAKA2013,
 AUTHOR={Iitaka, Shigeru},
 TITLE={Ring Theory (in {J}apanese)},
 PUBLISHER={Kyoritsu Shuppan Co., Ltd.},
 YEAR={2013}}


@BOOK{Leibniz1879,
  TITLE = {Explication de l'Arithm{\'e}tique Binaire},
  AUTHOR = {Leibniz, Gottfried Wilhelm},
  PUBLISHER = {C. Gerhardt},
  YEAR = {223 pages, 1879},
  VOLUME = {7},
  EDITION = {{D}ie {M}athematische {S}chriften}}

@ARTICLE{SmetsMagrez1987,
  TITLE = {Implication in Fuzzy Logic},
  AUTHOR = {Smets, Philippe and Magrez, Paul},
  JOURNAL = {International Journal of Approximate Reasoning},
  VOLUME = {1},
  NUMBER = {4},
  PAGES = {327--347},
  DOI = {10.1016/0888-613X(87)90023-5},
  YEAR = {1987}}


@Article{bsl0,
	title = {About a Certain Generalization of the Affine Ratio of Three Points and Unharmonic Ratio of Four Points},
	author = {Knop, Jadwiga},
	journal = {Bulletin of the Section of Logic},
	volume = {32},
	number = {1--2},
	pages = {33--42},
	year = {2003}}

@inproceedings{nakasho2015documentation,
  title={Documentation generator focusing on symbols for the {HTML}-ized {M}izar library},
  author={Nakasho, Kazuhisa and Shidama, Yasunari},
  booktitle={Intelligent Computer Mathematics, CICM 2015},
  volume={9150},
  series={Lecture Notes in Computer Science},
  editor={Kerber, Manfred and Carette, Jacques and Kaliszyk, Cezary and Rabe, Florian and Sorge, Volker},
  pages={343--347},
  year={2015},
  doi = {10.1007/978-3-319-20615-8\_25},
  organization={Springer, Cham}}

@article{papadopoulos2012remark,
  title={A remark on the projective geometry of constant curvature spaces},
  author={Papadopoulos, Athanase and Yamada, Sumio},
  journal={arXiv preprint arXiv:1209.3579},
url = {https://arxiv.org/pdf/1209.3579.pdf},
  year={2012}}

@article{kornilowicz2009define,
  title={How to define terms in {M}izar effectively},
  author={Korni{\l}owicz, Artur},
  journal={Studies in Logic, Grammar and Rhetoric},
  volume={18},
  pages={67--77},
  url={http://logika.uwb.edu.pl/studies/download.php?volid=31&artid=ak&format=PDF},
  year={2009}}

@ARTICLE{Lame:1844,
       AUTHOR = {Gabriel Lam\'{e}},
        TITLE = {Note sur la limite du nombre des divisions
        dans la recherche du plus grand commun diviseur entre
        deux nombres entiers},
      JOURNAL = {Comptes Rendus Acad. Sci.},
         YEAR = {1844},
       VOLUME = {19},
        PAGES = {867--870}}


@article{papadopoulos2015projective,
  title={On the projective geometry of constant curvature spaces},
  author={Papadopoulos, Athanase and Yamada, Sumio},
  journal={Sophus Lie and Felix Klein: The Erlangen Program and Its Impact in Mathematics and Physics},
  volume={23},
  pages={237--245},
  year={2015},
  publisher={Erich Schmidt Verlag GmbH \& Co. KG}}

@BOOK{Sneddon1957,
  TITLE = {Elements of Partial Differential Equations},
  AUTHOR = {Sneddon, Ian Naismith},
  PUBLISHER = {Tokyo McGraw-Hill Kogakusha, pages 209--273},
  YEAR = {1957}}

@BOOK{Fritz1990,
  TITLE = {Nonlinear Wave Equations, Formulation of Singularities},
  AUTHOR = {Fritz, John},
  PUBLISHER = {American Mathematical Society},
  YEAR = {1990},
  ISBN = {978-0-8218-7001-3}}

@BOOK{Nakao1992,
  TITLE = {Bibun-sekibun-gaku ({J}apanese)},
  AUTHOR = {Nakao, Mitsuhiro},
  PUBLISHER = {Kindai-kagaku-sha, pages 52--53},
  YEAR = {1992}}

@BOOK{Yano1982,
  TITLE = {Kaiseki-gaku-gairon ({J}apanese)},
  AUTHOR = {Yano, Kentaro},
  PUBLISHER = {Shokabo Co., Ltd.},
  YEAR = {1982}}

@inproceedings{GrabowskiCoghetto:2016,
  author    = {Grabowski, Adam and Coghetto, Roland},
  title     = {Tarski's Geometry and the {E}uclidean Plane in {M}izar},
  booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral
 Program, and Work in Progress at the Conference on Intelligent Computer
 Mathematics 2016 co-located with the 9th Conference on Intelligent
 Computer Mathematics {(CICM} 2016), Bia{\l}ystok, Poland, July 25--29,
 2016},
  pages     = {4--9},
  series = {CEUR-WS},
  volume = {1785},
  year      = {2016},
  publisher = {CEUR-WS.org},
  url       = {http://ceur-ws.org/Vol-1785/F2.pdf}}

@article{boutry2019parallel,
  title={Parallel postulates and continuity axioms: a
  mechanized study in intuitionistic logic using {C}oq},
  author={Boutry, Pierre and Gries, Charly and Narboux, Julien and Schreck, Pascal},
  journal={Journal of Automated Reasoning},
  volume={62},
  number={1},
  pages={1--68},
  year={2019},
  publisher={Springer}}

@Article{Beeson2019,
author={Beeson, Michael and Narboux, Julien and Wiedijk, Freek},
title={Proof-checking {E}uclid},
journal={Annals of Mathematics and Artificial Intelligence},
year={2019},
month={Jan},
day={10},
issn={1573-7470},
doi={10.1007/s10472-018-9606-x},
url={https://doi.org/10.1007/s10472-018-9606-x}}

@InProceedings{10.1007/978-3-540-77356-6_9,
  author={Narboux, Julien},
  editor={Botana, Francisco and Recio, Tomas},
  title={Mechanical Theorem Proving in {T}arski's Geometry},
  booktitle={Automated Deduction in Geometry},
  year={2007},
  publisher={Springer Berlin Heidelberg},
  address={Berlin, Heidelberg},
  pages={139--156},
  isbn={978-3-540-77356-6}}


@article{boutry:hal-01483457,
  TITLE = {{Formalization of the Arithmetization of {E}uclidean Plane Geometry and Applications}},
  AUTHOR = {Boutry, Pierre and Braun, Gabriel and Narboux, Julien},
  URL = {https://hal.inria.fr/hal-01483457},
  JOURNAL = {Journal of Symbolic Computation},
  PUBLISHER = {Elsevier},
  SERIES = {Special Issue on Symbolic Computation in Software Science},
  VOLUME = {90},
  PAGES = {149--168},
  YEAR = {2019},
  DOI = {10.1016/j.jsc.2018.04.007},
  PDF = {https://hal.inria.fr/hal-01483457/file/extended-arithmetization.pdf},
  HAL_ID = {hal-01483457},
  HAL_VERSION = {v1}}

@BOOK{Jac85,
      AUTHOR = {Jacobson, Nathan},
      TITLE = {Basic Algebra {I}},
      PUBLISHER = {Dover Books on Mathematics},
      YEAR = {1985}}

@book{sierpinski1965,
  title = {Cardinal and ordinal numbers},
  series = {Polska Akademia Nauk. Monografie matematyczne, (34) (in Polish)},
  author = {Sierpi{\'n}ski, Wac{\l}aw},
  address = {Warszawa},
  publisher = {PWN},
  year = {1965},
  edition = {2. ed., rev},
  pages = {491 pages}}

@book{Bachmann,
  title = {Transfinite Zahlen},
  series = {Ergebnisse der Mathematik und ihrer Grenzgebiete, (1)},
  author = {Bachmann, Heinz},
  address = {Berlin},
  publisher = {Springer},
  year = {1967},
  edition = {2., neubearb. Aufl.},
  pages = {VIII, 228}}

@article{Cantor,
  title={Beitr{\"a}ge zur Begr{\"u}ndung der transfiniten Mengenlehre},
  author={Cantor, Georg},
  journal={Mathematische Annalen},
  volume={49},
  number={2},
  pages={207--246},
  year={1897},
  publisher={Springer}}

@book{Abian,
  title = {The theory of sets and transfinite arithmetic},
  series = {Saunders Mathematics Books},
  author = {Abian, Alexander},
  address = {Philadelphia},
  publisher = {Saunders},
  year = {1965},
  pages = {406}}

@book{Deiser,
  title = {Einf{\"u}hrung in die Mengenlehre: die Mengenlehre {G}eorg {C}antors und ihre Axiomatisierung durch {E}rnst {Z}ermelo},
  author = {Deiser, Oliver},
  address = {Berlin},
  publisher = {Springer},
  year = {2004},
  edition = {2., verb. und erw. Aufl.},
  ISBN = {3-540-20401-6},
  pages = {551}}

@inproceedings{GomolinskaRIF2008,
author = {Gomoli\'nska, Anna},
title = {On certain rough inclusion functions},
editor={Peters, James F. and Skowron, Andrzej and Rybi{\'{n}}ski, Henryk},
booktitle = {Transactions on Rough Sets IX},
series = {Lecture Notes in Computer Science}, 
volume = {5390}, 
publisher = {Springer Berlin Heidelberg},
pages = {35--55},
year = 2008,
doi = {10.1007/978-3-540-89876-4\_3}}

@inproceedings{GomolinskaRIF2007,
author = {Gomoli\'nska, Anna},
title = {On Three Closely Related Rough Inclusion Functions},
editor={Kryszkiewicz, Marzena and Peters, James F. and Rybi{\'n}ski, Henryk and Skowron, Andrzej},
booktitle={Rough Sets and Intelligent Systems Paradigms},
series = {Lecture Notes in Computer Science},
volume = {4585},
year = {2007},
pages = {142--151},
publisher = {Springer},
address = {Berlin, Heidelberg},
doi = {10.1007/978-3-540-73451-2\_16}}

@inproceedings{KinyonVV13,
  author    = {Kinyon, Michael K. and Veroff, Robert and Vojt{\v{e}}chovsk{\'{y}}, Petr},
  title     = {Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction},
  booktitle = {Automated Reasoning and Mathematics -- Essays in Memory of William W. McCune},
  pages     = {151--164},
  year      = {2013},
  crossref  = {2013mccune}}

@proceedings{2013mccune,
  editor    = {Bonacina, Maria Paola and Stickel, Mark E.},
  title     = {Automated Reasoning and Mathematics -- Essays in Memory of {W}illiam {W}. {M}c{C}une},
  series    = {Lecture Notes in Computer Science},
  volume    = {7788},
  publisher = {Springer},
  year      = {2013}}

@ARTICLE{Albert43,
  AUTHOR =       {Albert, A. A.},
  TITLE =        {{Q}uasigroups. {I}},
  JOURNAL =      {Transactions of the American Mathematical Society},
  YEAR =         {1943},
  volume =       {54},
  number =       {3},
  pages =        {507--519},
  publisher =    {American Mathematical Society}}

@book{AGT,
  title={Algebraic graph theory: morphisms, monoids and matrices},
  author={Knauer, Ulrich},
  series = {De Gruyter Studies in Mathematics},
  volume={41},
  year={2011},
  publisher={Walter de Gruyter}}

@book{HOMO,
  title = {Graphs and homomorphisms},
  series = {Oxford Lecture Series in Mathematics and Its Applications; 28},
  author = {Hell, Pavol and Nesetril, Jaroslav},
  address = {Oxford},
  publisher = {Oxford University Press},
  year = {2004},
  ISBN = {0-19-852817-5},
  pages = {IX, 244},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?12385357_toc.pdf}{\tt http://scans.hebis.de/HEBCGI/show.pl?12385357_toc.pdf}},
  url = {http://scans.hebis.de/HEBCGI/show.pl?12385357_toc.pdf}}

@book{COLPROB,
  title = {Graph coloring problems},
  series = {Wiley-Interscience Series in Discrete Mathematics and Optimization},
  author = {Jensen, Tommy R. and Toft, Bjarne},
  address = {New York},
  publisher = {Wiley},
  year = {1995},
  ISBN = {0-471-02865-7},
  pages = {XIX, 295},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?04673951_toc.pdf}{\tt http://scans.hebis.de/HEBCGI/show.pl?04673951_toc.pdf}},
  url = {http://scans.hebis.de/HEBCGI/show.pl?04673951_toc.pdf}}

@book{AGT2,
  title = {Algebraic graph theory},
  series = {Graduate Texts in Mathematics; 207},
  author = {Godsil, Christopher David and Royle, Gordon},
  address = {New York},
  publisher = {Springer},
  year = {2001},
  ISBN = {0-387-95220-9; 0-387-95241-1},
  pages = {XIX, 439},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?09922696_ein-1.pdf}{\tt http://scans.hebis.de/HEBCGI/show.pl?09922696_ein-1.pdf}},
  url = {http://scans.hebis.de/HEBCGI/show.pl?09922696_ein-1.pdf}}

@book{CAYLEY,
  title = {Expander families and {C}ayley graphs: a beginners guide},
  author = {Krebs, Mike and Shaheen, Anthony},
  address = {Oxford},
  publisher = {Oxford University Press},
  year = {2011},
  ISBN = {0-19-976711-4; 978-0-19-976711-3},
  pages = {XXIV, 258}}

@book{EXPATH,
  title = {Extremal paths in graphs: foundations, search strategies, and related topics},
  series = {Mathematical Topics},
  volume = {10},
  author = {Huckenbeck, Ulrich},
  address = {Berlin},
  publisher = {Akademie Verlag},
  year = {1997},
  edition = {1.},
  ISBN = {3-05-501658-0; 978-3-05-501658-5},
  pages = {480},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?05834025_toc.pdf}{\tt http://scans.hebis.de/HEBCGI/show.pl?05834025_toc.pdf}},
  url = {http://scans.hebis.de/HEBCGI/show.pl?05834025_toc.pdf}}

@book{DISC,
  title = {A first course in discrete mathematics},
  series = {Springer Undergraduate Mathematics Series},
  author = {Anderson, Ian},
  address = {London},
  publisher = {Springer},
  year = {2001},
  ISBN = {1-85233-236-0},
  pages = {VIII, 200},
   NOTE = {\href{http://scans.hebis.de/HEBCGI/show.pl?09315030_vlg.html}{\tt http://scans.hebis.de/HEBCGI/show.pl?09315030_vlg.html}},
  url = {http://scans.hebis.de/HEBCGI/show.pl?09315030_vlg.html}}

@Inproceedings{Gomolinska2009,
  author={Gomoli{\'{n}}ska, Anna},
  editor={Peters, James F. and Skowron, Andrzej and Wolski, Marcin
  and Chakraborty, Mihir K. and Wu, Wei-Zhi},
  title={Rough Approximation Based on Weak q-{RIF}s},
  bookTitle={Transactions on Rough Sets X},
  series = {Lecture Notes in Computer Science}, 
  volume = {5656}, 
  year={2009},
  publisher={Springer},
  address={Berlin, Heidelberg},
  pages={117--135},
  isbn={978-3-642-03281-3},
  doi={10.1007/978-3-642-03281-3_4},
  url={https://doi.org/10.1007/978-3-642-03281-3_4}}

@InProceedings{GrabowskiIJCRS2019,
  author={Grabowski, Adam},
  editor={Mih{\'a}lyde{\'a}k, Tam{\'a}s and Min, Fan and Wang, Guoyin
  and Banerjee, Mohua and D{\"u}ntsch, Ivo and Suraj, Zbigniew and Ciucci, Davide},
  title={Building a Framework of Rough Inclusion Functions by Means of Computerized Proof Assistant},
  booktitle={Rough Sets},
  year={2019},
  publisher={Springer International Publishing},
  series={Lecture Notes in Computer Science}, 
  volume={11499},
  address={Cham},
  pages={225--238},
  isbn={978-3-030-22815-6},
  doi={10.1007/978-3-030-22815-6_18},
  url ={https://doi.org/10.1007/978-3-030-22815-6_18}}

@INProceedings{PolkowskiRM2011,
  author={Polkowski, Lech},
  title={Rough Mereology},
  booktitle={Approximate Reasoning by Parts},
  series = {Intelligent Systems Reference Library},
  volume = {20},
  year={2011},
  publisher={Springer},
  address={Berlin, Heidelberg},
  pages={229--257},
  isbn={978-3-642-22279-5},
  doi={10.1007/978-3-642-22279-5_6}}

@ARTICLE{PolkowskiS:1996,
  AUTHOR =       {Polkowski, Lech and Skowron, Andrzej},
  TITLE =        {Rough Mereology: A New Paradigm for Approximate Reasoning},
  JOURNAL =      {International Journal of Approximate Reasoning},
  YEAR =         {1996},
  volume =       {15},
  number =       {4},
  pages =        {333--365},
  doi = {10.1016/S0888-613X(96)00072-2}}

@INCOLLECTION{Lukasiewicz:1913, 
author = {{\L}ukasiewicz, Jan}, 
title = {Die logischen {G}rundlagen der {W}ahrscheinlichkeitsrechnung}, 
booktitle = {Jan {\L}ukasiewicz -- {S}elected {W}orks}, 
editor = {Borkowski, L.}, 
publisher = {North Holland, Polish Scientific Publ.},   
address = {Amsterdam London Warsaw}, 
pages = {16--63}, 
year = {1970},  
note = {First published in Krak\'{o}w, 1913}} 

@inproceedings{Mehta:1991,
 author={Mayur Mehta and Vijay Parmar and Earl Swartzlander},
 booktitle={{P}roceedings 10th {IEEE} Symposium on Computer Arithmetic},
 title={High-speed Multiplier Design using Multi-input Counter and Compressor Circuits},
 year={1991},
 volume={},
 number={},
 pages={43--50},
 doi={10.1109/ARITH.1991.145532},
 month={June}}

@article{Wallace:1964,
 author={Christopher Stewart Wallace},
 journal={{IEEE} Transactions on Electronic Computers},
 title={A Suggestion for a Fast Multiplier},
 year={1964},
 volume={EC-13},
 number={1},
 pages={14--17},
 doi={10.1109/PGEC.1964.263830}}

@article{Vuillemin:1983,
 author = {Jean Vuillemin},
 title = {A Very Fast Multiplication Algorithm for {VLSI} Implementation},
 journal = {Integration},
 volume = {1},
 number = {1},
 pages = {39--52},
 year = {1983},
 issn = {0167-9260},
 doi = {10.1016/0167-9260(83)90005-6}}

@inproceedings{Iwasaki:2008,
 author    = {Naoki Iwasaki and Katsumi Wasaki},
 title     = {A Meta Hardware Description Language Melasy for Model-Checking Systems},
 booktitle = {Proceedings 5th International Conference on Information Technology: New Generations
              {(ITNG} 2008)},
 pages     = {273--278},
 year      = {2008},
 doi       = {10.1109/ITNG.2008.135}}

@book{Garey:1979,
 author = {Garey, Michael R. and Johnson, David S.},
 title = {Computers and Intractability: A Guide to the Theory of {NP}-Completeness},
 year = {1979},
 isbn = {0716710447},
 publisher = {W. H. Freeman \& Co.},
 address = {New York, NY, USA}}

@inproceedings{Karp1972,
author={Karp, Richard M.},
title={Reducibility among Combinatorial Problems},
year={1972},
pages={85--103},
isbn={978-1-4684-2001-2},
doi={10.1007/978-1-4684-2001-2_9},
url={https://doi.org/10.1007/978-1-4684-2001-2_9},
publisher={Springer US},
crossref  = {Complexity:1972}}

@proceedings{Complexity:1972,
editor={Miller, Raymond E. and Thatcher, James W. and Bohlinger, Jean D.},
title={Complexity of Computer Computations},
booktitle={Complexity of Computer Computations},
year={1972},
publisher={Springer US},
pages={85--103},
isbn={978-1-4684-2001-2},
doi={10.1007/978-1-4684-2001-2_9},
url={https://doi.org/10.1007/978-1-4684-2001-2_9}}

@BOOK{Sierpinski:1970,
 AUTHOR={Sierpi{\'n}ski, Wac{\l}aw},
 TITLE={250 Problems in Elementary Number Theory},
 PUBLISHER={Elsevier},
   NOTE = {\url{https://www.isinj.com/mt-aime/250 Problems in Elementary Number Theory - Sierpinski (1970).pdf}},
 YEAR={1970}}

@book{GERDIE,
  title = {Graphentheorie},
  author = {Diestel, Reinhard},
  address = {Heidelberg},
  publisher = {Springer-Lehrbuch Masterclass},
  year = {2012},
  edition = {4. Aufl. 2010. 3., korr. Nachdruck},
  ISBN = {978-3-642-14911-5}}

@inproceedings{CBKP-CICM/MKM19,
  author    = {Brown, Chad E. and P\k{a}k, Karol},
  editor    = {Kaliszyk, Cezary and
               Brady, Edwin and
               Kohlhase, Andrea and
               Sacerdoti Coen, Claudio},
  title     = {A Tale of Two Set Theories},
  booktitle = {Intelligent Computer Mathematics -- 12th International Conference,
               {CICM} 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings},
  series    = {Lecture Notes in Computer Science},
  pages     = {44--60},
  year      = {2019},
  volume    = {11617},
  publisher = {Springer},
  doi       = {10.1007/978-3-030-23250-4_4}}

@inproceedings{Schw18,
	author={Schwarzweller, Christoph},
	pages={67--72},
	title={Representation Matters: An Unexpected Property of Polynomial Rings and its Consequences for Formalizing Abstract Field Theory},
	booktitle={Proceedings of the 2018 Federated Conference on Computer Science and Information Systems},
	year={2018},
	editor={Ganzha, M. and Maciaszek, L. and Paprzycki, M.},
	publisher={IEEE},
	doi={10.15439/2018F88},
	url={http://dx.doi.org/10.15439/2018F88},
	volume={15},
	series={Annals of Computer Science and Information Systems}}

@article{NASH,
  title={Infinite Graphs -- A Survey},
  author={Nash-Williams, C. St. J. A.},
  journal={Journal of Combinatorial Theory},
  volume={3},
  number={3},
  pages={286--301},
  year={1967},
  publisher={Academic Press}}

@book{DIEST,
  title = {Graph Theory},
  series = {Graduate Texts in Mathematics; 173},
  author = {Diestel, Reinhard},
  address = {New York},
  publisher = {Springer},
  year = {2000},
  edition = {2nd},
  ISBN = {0-387-98976-5; 0-387-98976-5},
  pages = {XIV, 312 S.}}

@book{HANDBOOK,
  title = {Handbook of Discrete and Combinatorial Mathematics},
  series = {Discrete Mathematics and Its Applications},
  editor = {Rosen, Kenneth H.},
  address = {Boca Raton},
  publisher = {CRC Press},
  year = {2018},
  edition = {Second},
  ISBN = {978-1-58488-780-5},
  pages = {xxiv, 1590 Seiten}}

@book{GRELAT,
  title={Relations and Graphs: Discrete Mathematics for Computer Scientists},
  author={Schmidt, Gunther and Str{\"o}hlein, Thomas},
  year={2012},
  publisher={Springer Science \& Business Media}}

@article{pak2014improving,
  title={Improving legibility of natural deduction proofs is not trivial},
  author={P\k{a}k, Karol},
  journal={Logical Methods in Computer Science},
  volume={10},
  year={2014},
  publisher={Episciences.org}}

@article{Williams:1969,
     author = {Williams, N. H.},
     title = {On {G}rothendieck universes},
     journal = {Compositio Mathematica},
     publisher = {Wolters-Noordhoff Publishing},
     volume = {21},
     number = {1},
     year = {1969},
     pages = {1-3},
     zbl = {0175.00701},
     mrnumber = {244035},
     language = {en},
     url = {http://www.numdam.org/item/CM_1969__21_1_1_0}}

@INPROCEEDINGS{Vernacular2006,
  author = {Grabowski, Adam and Schwarzweller, Christoph},
  title = {{T}ranslating mathematical vernacular into knowledge repositories},
  booktitle     = {Mathematical Knowledge Management},
  note = {4th International Conference on Mathematical Knowledge Management, Bremen, Germany, MKM 2005, July 15--17, 2005, Revised Selected Papers},
  pages     = {49--64},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3863},
  year      = {2006},
  DOI = {10.1007/11618027_4},
  EDITOR = {Kohlhase, Michael}}

@article{coquand2014theorie,
  title={Th{\'e}orie des types d{\'e}pendants et axiome d'univalence},
  author={Coquand, Thierry},
  journal={S{\'e}minaire Bourbaki},
  volume={66},
  pages={1085},
  year={2014}}

@article{tabareau2018equivalences,
  title={Equivalences for free: univalent parametricity for effective transport},
  author={Tabareau, Nicolas and Tanter, {\'E}ric and Sozeau, Matthieu},
  journal={Proceedings of the ACM on Programming Languages},
  volume={2},
  number={ICFP},
  pages={1--29},
  year={2018},
  publisher={ACM New York, NY, USA}}

@inproceedings{johnsen2004theorem,
  title={Theorem reuse by proof term transformation},
  author={Johnsen, Einar Broch and L{\"u}th, Christoph},
  booktitle={International Conference on Theorem Proving in Higher Order Logics},
  pages={152--167},
  year={2004},
  publisher={Springer}}

@inproceedings{huffman2013lifting,
  title={Lifting and Transfer: A modular design for quotients in {I}sabelle/{HOL}},
  author={Huffman, Brian and Kun{\v{c}}ar, Ond{\v{r}}ej},
  booktitle={International Conference on Certified Programs and Proofs},
  pages={131--146},
  year={2013},
  publisher={Springer}}

@article{zimmermann2015automatic,
  title={Automatic and transparent transfer of theorems along isomorphisms in the {C}oq proof assistant},
  author={Zimmermann, Theo and Herbelin, Hugo},
  journal={arXiv preprint arXiv:1505.05028},
  year={2015}}

@inproceedings{magaud2003changing,
  title={Changing data representation within the {C}oq system},
  author={Magaud, Nicolas},
  booktitle={International Conference on Theorem Proving in Higher Order Logics},
  pages={87--102},
  year={2003},
  publisher={Springer}}

@Inbook{Grabowski2020,
author={Grabowski, Adam and Korni{\l}owicz, Artur and Schwarzweller, Christoph},
editor={Grabowski, Adam and Loukanova, Roussanka and Schwarzweller, Christoph},
title={Refining Algebraic Hierarchy in Mathematical Repository of {M}izar},
bookTitle={{AI} Aspects in Reasoning, Languages, and Computation},
year={2020},
publisher={Springer},
address={Cham},
pages={49--75},
isbn={978-3-030-41425-2},
doi={10.1007/978-3-030-41425-2_2},
url={https://doi.org/10.1007/978-3-030-41425-2_2}}

@Inbook{Grabo2020EFT,
author={Grabowski, Adam and Coghetto, Roland},
editor={Grabowski, Adam and Loukanova, Roussanka and Schwarzweller, Christoph},
title={Extending Formal Topology in Mizar by Uniform Spaces},
bookTitle={{AI} Aspects in Reasoning, Languages, and Computation},
year={2020},
publisher={Springer},
address={Cham},
pages={77--105},
isbn={978-3-030-41425-2},
doi={10.1007/978-3-030-41425-2_2},
url={https://doi.org/10.1007/978-3-030-41425-2_2}}

@proceedings{chad-brown:2019-3548609,
  author       = {Brown, Chad E. and Kaliszyk, Cezary and P\k{a}k, Karol},
  title        = {Higher-Order {T}arski {G}rothendieck as a Foundation for Formal Proof},
  year         = {2019},
  publisher    = {Zenodo},
  month        = {Sep.},
  doi          = {10.4230/lipics.itp.2019.9},
  url          = {https://doi.org/10.4230/lipics.itp.2019.9}}

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

@BOOK{takagi1983,
      AUTHOR = {Takagi, Teiji},
      TITLE = {Introduction to Analysis},
      edition = {3rd},
      PUBLISHER = {Iwanami Shoten, Publishers},
      YEAR = {1983}}

@BOOK{Vajda:2007,
      AUTHOR = {Vajda, Steven},
      TITLE = {Fibonacci \& Lucas Numbers, and 
      the Golden Section: Theory and Applications},
      PUBLISHER = {Dover Publications},
      ISBN = {978-0486462769},
      YEAR = {2007}}

@BOOK{Koshy:2017,
      AUTHOR = {Koshy, Thomas},
      TITLE = {Fibonacci and {L}ucas Numbers with Applications, 
    Volume 1},
      PUBLISHER = {John Wiley \& Sons, Inc.},
      DOI = {10.1002/9781118742327},
      ISBN = {978-1118742129},
      YEAR = {2017}}

@article{Kornilowicz:2015:FC,
author = {Korni{\l}owicz, Artur},
title = {Flexary Connectives in {M}izar},
journal = {Computer Languages, Systems \& Structures},
year = {2015},
volume = {44},
issue = {Part C},
pages = {238--250},
month = {December},
publisher = {Elsevier},
url = {http://dx.doi.org/10.1016/j.cl.2015.07.002},
doi = {10.1016/j.cl.2015.07.002}}

@article{Mamdani:1974,
author = {Mamdani, Ebrahim H.},
title = {Application of Fuzzy Algorithms for Control of Simple Dynamic Plant},
journal = {IEE Proceedings},
year = {1974},
volume = {121},
issue = {12},
pages = {1585--1588},
url = {https://ci.nii.ac.jp/naid/20000916707/}}

@InProceedings{Mitsuishi:2012,
author = {Mitsuishi, Takashi and Terashima, Takanori and  Shimada, Nami and Homma, Toshimichi and Sawada, Kiyoshi and Shidama, Yasunari},
title = {Continuity of defuzzification on {L$^2$} space for optimization of fuzzy control},
booktitle = {Active Media Technology},
year = {2012},
publisher = {Springer-Berlin-Heidelberg},
pages = {73--81},
isbn = {978-3-642-35236-2}}

@INPROCEEDINGS{Mitsuishi:2015,
author = {Mitsuishi, Takashi and Shimada, Nami and Homma, Toshimichi and Ueda, Mayumi and Kochizawa, Masayuki and Shidama, Yasunari},
title = {Continuity of approximate reasoning using fuzzy number under {{\L}}ukasiewicz t-norm},
year = {2015},
booktitle = {2015 IEEE 7th International Conference on Cybernetics and Intelligent Systems (CIS) and IEEE Conference on Robotics, Automation and Mechatronics (RAM)},
pages = {71--74},
doi = {10.1109/ICCIS.2015.7274550}}

@INPROCEEDINGS{Mitsuishi:2018,
author = {Mitsuishi, Takashi},
title = {Uncertain Defuzzified Value of Periodic Membership Function},
booktitle = {2018 International Electrical Engineering Congress (iEECON)},
year = {2018},
pages = {1--4},
doi = {10.1109/IEECON.2018.8712319}}

@BOOK{Lang2002,
      AUTHOR = {Lang, Serge},
      TITLE = {Algebra ({R}evised {T}hird {E}dition)},
      PUBLISHER = {Springer Verlag},
      YEAR = {2002}}

@book{KorteVygen2012,
 author = {Korte, B. and Vygen, J.},
 title = {Combinatorial Optimization: Theory and Algorithms},
 year = {2012},
 isbn = {3642244874, 9783642244872},
 edition = {5th},
 publisher = {Springer Publishing Company, Incorporated}}

@book{Johnson1973,
  title={Near-optimal Bin Packing Algorithms},
  author={Johnson, David S.},
  series={PhD thesis},
  year={1973},
  publisher={Massachusetts Institute of Technology}}

@BOOK{READSIMON1980,
      AUTHOR = {Read, Michael and Simon, Barry},
      TITLE = {Functional Analysis ({M}ethods of Modern Mathematical Physics)},
      PUBLISHER = {Academic Press},
      YEAR = {1980}}

@BOOK{Lang:1993,
      AUTHOR = {Lang, Serge},
      TITLE = {Real and Functional Analysis ({T}exts in Mathematics)},
      PUBLISHER = {Springer-Verlag},
      YEAR = {1993}}

@BOOK{Matsuzaka:2000,
      AUTHOR = {Matsuzaka, Kazuo},
      TITLE = {Sets and Topology ({I}ntroduction to Mathematics)},
      PUBLISHER = {IwanamiShoten},
      YEAR = {2000}}

@article{Ozawa:2012,  
  TITLE = {Ascoli-{A}rzel{\`a} theorem},
  AUTHOR = {Ozawa, Tohru},
  URL = {http://www.ozawa.phys.waseda.ac.jp/pdf/Ascoli.pdf},
  PDF = {http://www.ozawa.phys.waseda.ac.jp/pdf/Ascoli.pdf},
  YEAR = {2012}}

@article{Schweigert:1982,
  title={Near Lattices},
  author={Schweigert, Dietmar},
  journal={Mathematica Slovaca},
  volume={32},
  number={3},
  pages={313--317},
  year={1982}}

@article{FriedGratzer:1973,
  title={Some Examples of Weakly Associative Lattices},
  author={Fried, Ervin and Gr\"atzer, George},
  journal={Colloquium Mathematicum},
  volume={27},
  pages={215--221},
  year={1973},
  doi = {10.4064/cm-27-2-215-221}}

@ARTICLE{AMM76,
  AUTHOR =       {Jones, James P. and Daihachiro, Sato and Wada, Hideo and Wiens, Douglas},
  TITLE =        {Diophantine Representation of the Set of Prime Numbers},
  JOURNAL =      {The American Mathematical Monthly},
  YEAR =         {1976},
  volume =       {83},
  number =       {6},
  pages =        {449--464}}

@book{hartshorne1967foundations,
  title={Foundations of Projective Geometry},
  author={Hartshorne, Robin},
  year={1967},
  publisher={Citeseer}}

@book{coxeter1992real,
  title={The Real Projective Plane},
  author={Coxeter, Harold Scott Macdonald},
  year={1992},
  publisher={Springer Science \& Business Media}}

@inproceedings{buchholtz2017real,
  title={The real projective spaces in homotopy type theory},
  author={Buchholtz, Ulrik and Rijke, Egbert},
  booktitle={32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  pages={1--8},
  year={2017},
  organization={IEEE}}

@article{Projective_Geometry-AFP,
  author  = {Bordg, Anthony},
  title   = {Projective Geometry},
  journal = {Archive of Formal Proofs},
  month   = {jun},
  year    = {2018},
  url    = {https://isa-afp.org/entries/Projective_Geometry.html},
  ISSN    = {2150-914x}}

@article{magaud2012case,
  title={A case study in formalizing projective geometry in {C}oq: {D}esargues theorem},
  author={Magaud, Nicolas and Narboux, Julien and Schreck, Pascal},
  journal={Computational Geometry},
  volume={45},
  number={8},
  pages={406--424},
  year={2012},
  publisher={Elsevier}}

@phdthesis{braun2019approche,
  title={Approche combinatoire pour l'automatisation en {C}oq des preuves formelles en g{\'e}om{\'e}trie d'incidence projective},
  author={Braun, David},
  year={2019},
  school={Universit{\'e} de Strasbourg}}

@article{calderon2018formalizing,
  title={Formalizing Constructive Projective Geometry in {A}gda},
  author={Calder{\'o}n, Guillermo},
  journal={Electronic Notes in Theoretical Computer Science},
  volume={338},
  pages={61--77},
  year={2018},
  publisher={Elsevier}}

@article{Jones1982,
  title={Universal Diophantine Equation},
  author={Jones, James P.},
  journal={Journal of Symbolic Logic},
  year={1982},
  volume={47},
  NUMBER={4},
  pages={549--571}}

@article{sun2021results,
      title={Further results on {H}ilbert's {T}enth {P}roblem},
      author={Sun, Zhi-Wei},
      year={2021},
    JOURNAL = {Science China Mathematics},
      VOLUME = {64},
    PAGES = {281--306},
    DOI = {10.1007/s11425-020-1813-5}}

@ARTICLE{MR75,
  AUTHOR =       {Matiyasevich, Yuri and Robinson, Julia},
  TITLE =        {Reduction of an Arbitrary Diophantine Equation to One in 13 Unknowns},
  JOURNAL =      {Acta Arithmetica},
  YEAR =         {1975},
  volume =       {27},
  pages =        {521--553}}

@article{Matiyasevich81,
      title={Primes are Nonnegative Values of a Polynomial in 10 Variables},
      author={Matiyasevich, Yuri},
      year={1981},
    JOURNAL = {Journal of Soviet Mathematics},
      VOLUME = {15},
    PAGES = {33--44},
    DOI = {10.1007/BF01404106}}

@article{Jones1979DiophantineRO,
  title={Diophantine representation of {M}ersenne and {F}ermat primes},
  author={Jones, James P.},
  journal={Acta Arithmetica},
  year={1979},
  volume={35},
  pages={209--221},
  DOI = {10.4064/AA-35-3-209-221}}

@article{GrauTBA:1947,
  author = {Grau, Albert A.},
  title = {Ternary {B}oolean algebra},
  volume = {53},
  journal = {Bulletin of the American Mathematical Society},
  number = {6},
  publisher = {American Mathematical Society},
  pages = {567--572},
  year = {1947},
  doi = {bams/1183510797}}

@article{PadmanabhanTBA:1995,
  author = {Padmanabhan, Ranganathan and McCune, William},
  journal = {Computers and Mathematics with Applications},
  volume = {29}, 
  number = {2}, 
  pages = {13--16},
  publisher = {Elsevier},
  year = {1995}}

@Book{vanDalen:2013,
 Author = {van Dalen, Dirk},
 Title = {Logic and Structure},
 FJournal = {Universitext},
 Journal = {Universitext},
 ISSN = {0172-5939},
 ISBN = {978-1-4471-4557-8; 978-1-4471-4558-5},
 Pages = {x + 263},
 Year = {2013},
 Publisher = {London: Springer},
 Language = {English},
 DOI = {10.1007/978-1-4471-4558-5},
 MSC2010 = {03-01 03-02 03B05 03B10 03B15 03B20 03C07 03C20},
 Zbl = {1262.03002}}

@Book{TroelstraDalen:1988,
 Author = {Troelstra, Anne Sjerp and van Dalen, Dirk},
 Title = {Constructivism in Mathematics. {A}n Introduction. {V}olume {I}},
 Series = {Studies in Logic and the Foundations of Mathematics},
 Volume = {121},
 ISBN = {0-444-70506-6},
 Pages = {xv + 355},
 Year = {1988},
 Publisher = {Amsterdam etc.: North-Holland},
 Language = {English},
 MSC2010 = {03F50 03F55 03F60 03F65 03-02 03-01},
 Zbl = {0653.03040}}

@Book{Heyting:1971,
 Author = {Heyting, Arend},
 Title = {Intuitionism. An Introduction},
 Journal = {Studies in Logic and the Foundations of Mathematics},
 Year = {1971},
 Publisher = {Elsevier, Amsterdam, 3rd revised ed.},
 Language = {English},
 MSC2010 = {03F55 03-01},
 Zbl = {0219.02013}}


@BOOK{Rosenblatt1958,
  TITLE={The Perceptron: A Probabilistic Model for Information Storage and Organization
         in the Brain},
  AUTHOR={Rosenblatt, Frank},
  PUBLISHER={Psychological Review},
  YEAR={1958}}

@BOOK{Rumelhart1986,
  TITLE = {Learning Representations by Backpropagating Errors},
  AUTHOR = {Rumelhart, David Everett and Hinton, Geoffrey Everes and Williams, Ronald J.},
  PUBLISHER = {Nature},
  YEAR = {1986}}

@BOOK{Schmidhuber2015,
  TITLE = {Deep Learning in Neural Networks: An Overview},
  AUTHOR = {Schmidhuber, J{\"u}rgen},
  PUBLISHER = {Neural Networks},
  YEAR = {2015}}

@BOOK{Lang1993,
      AUTHOR = {Lang, Serge},
      TITLE = {Real and Functional Analysis (Texts in Mathematics)},
      PUBLISHER = {Springer-Verlag},
      YEAR = {1993}}

@book{dummit-foote:2004,
  title={{Abstract Algebra}},
  author={Dummit, David S. and Foote, Richard M.},
  edition={{Third}},
  year={2004},
  publisher={Wiley and Sons}}

@book{gorenstein:1980,
  title={{Finite Groups}},
  author={Gorenstein, Daniel},
  year={1980},
  edition={{Second}},
  publisher={Chelsea Publishing Company}}

@book{isaacs:2008,
  author={Isaacs, I.~Martin},
  title={{Finite Group Theory}},
  year={2008},
  publisher={American Mathematical Society},
  series={Graduate Studies in Mathematics},
  volume={92}}

@incollection{artin1963theorie,
  title={Th{\'e}orie des topos et cohomologie {\'e}tale des 
    sch{\'e}mas. {T}ome 1: {T}h{\'e}orie des topos (expos{\'e}s I {\`a} IV)},
  author={Artin, Michael and Grothendieck, Alexander and Verdier, Jean-Louis},
  booktitle={S{\'e}minaire de G{\'e}om{\'e}trie Alg{\'e}brique du Bois Marie, 1963/64, SGA 4},
  volume={269},
  series = {Lecture Notes in Mathematics},
  publisher = {Springer},
  year = {1972}} 

@book{Ross:2010,
author={Ross, Timothy J.},
title={Fuzzy Logic with Engineering Applications},
publisher={John Wiley and Sons Ltd},
year={2010}}

@article{Leekwijck:1999,
  title={Defuzzification: Criteria and Classification},
  author={Van Leekwijck, Werner and Kerre, Etienne E.},
  journal={Fuzzy Sets and Systems},
  volume={108},
  number={2},
  pages={159--178},
  year={1999},
  publisher={Elsevier}}

@article{Katafuchi:2001,
  title={Investigation of Deffuzification in Fuzzy Inference: Proposal of a New Defuzzification Method (in {J}apanese)},
  author={Katafuchi, Tetsuro and Asai, Kiyoji and Fujita, Hiroshi},
  journal={Medical Imaging and Information Sciences},
  volume={18},
  number={1},
  pages={19--30},
  year={2001},
  doi={10.11318/mii1984.18.19}}

@inproceedings{Mizumoto:1990,
  title={Improvement of Fuzzy Control ({IV})-Case by Product-sum-gravity Method},
  author={Mizumoto, Masaharu},
  booktitle={Proc. 6th Fuzzy System Symposium, 1990},
  pages={9--13},
  year={1990}}

@BOOK{AndersonFuller:1992,
 AUTHOR={Anderson, Frank W. and Fuller, Kent R.},
 TITLE={Rings and Categories of Modules, Second Edition},
 PUBLISHER={Springer-Verlag},
 YEAR={1992}} 

@book{DIESTEL,
  TITLE = {Graph Theory},
  VOLUME = {Graduate Texts in Mathematics; 173},
  AUTHOR = {Diestel, Reinhard},
  ADDRESS = {Berlin},
  PUBLISHER = {Springer},
  YEAR = {2017},
  EDITION = {Fifth},
  ISBN = {978-3-662-53621-6},
  PAGES = {XVIII, 428 p.}}

@misc{nlab:grothendieck_universe,
  author = {n{L}ab {A}uthors},
  title = {{G}rothendieck universe},
  url = {https://ncatlab.org/nlab/revision/Grothendieck%20universe/53},
  year = {2022}}

@book{lurie2009higher,
  title={Higher Topos Theory},
  author={Lurie, Jacob},
  year={2009},
  publisher={Princeton University Press}}

@article{caramello2021relative,
  title={Relative Topos Theory via Stacks},
  author={Caramello, Olivia and Zanfa, Riccardo},
  journal={arXiv preprint arXiv:2107.04417},
  year={2021}}

@article{shulman2008set,
  title={Set Theory for Category Theory},
  author={Shulman, Michael A.},
  journal={arXiv preprint arXiv:0810.1279},
  year={2008}}

@book{riehl2017category,
  title={Category Theory in Context},
  author={Riehl, Emily},
  year={2017},
  publisher={Courier Dover Publications}}

@article{gratzer2022strict,
  title={Strict Universes for {G}rothendieck Topoi},
  author={Gratzer, Daniel and Shulman, Michael and Sterling, Jonathan},
  journal={arXiv preprint arXiv:2202.12012},
  year={2022}}

@inproceedings{Naumowicz:2020,
  author    = {Naumowicz, Adam},
  editor    = {Christoph Benzm{\"{u}}ller and Bruce R. Miller},
  title     = {Dataset Description: Formalization of Elementary Number Theory in
               {M}izar},
  booktitle = {Intelligent Computer Mathematics -- 13th International Conference,
               {CICM} 2020, Bertinoro, Italy, July 26--31, 2020, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {12236},
  pages     = {303--308},
  publisher = {Springer},
  year      = {2020},
  url       = {https://doi.org/10.1007/978-3-030-53518-6\_22},
  doi       = {10.1007/978-3-030-53518-6\_22}}

@inproceedings{Grabowski:2021,
  author    = {Grabowski, Adam},
  title     = {Fuzzy Implications in the {M}izar System},
  booktitle = {30th {IEEE} International Conference on Fuzzy Systems, {FUZZ-IEEE}
               2021, Luxembourg, July 11--14, 2021},
  pages     = {1--6},
  publisher = {{IEEE}},
  year      = {2021},
  url       = {https://doi.org/10.1109/FUZZ45933.2021.9494593},
  doi       = {10.1109/FUZZ45933.2021.9494593}}

@inproceedings{DBLP:conf/itp/PakK22,
  author    = {P\k{a}k, Karol and Kaliszyk, Cezary},
  editor    = {June Andronick and Leonardo de Moura},
  title     = {Formalizing a Diophantine Representation of the Set of Prime Numbers},
  booktitle = {13th International Conference on Interactive Theorem Proving, {ITP}
               2022, August 7-10, 2022, Haifa, Israel},
  series    = {LIPIcs},
  volume    = {237},
  pages     = {26:1--26:8},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2022},
  url       = {https://doi.org/10.4230/LIPIcs.ITP.2022.26},
  doi       = {10.4230/LIPIcs.ITP.2022.26},
  timestamp = {Thu, 29 Sep 2022 08:36:57 +0200},
  biburl    = {https://dblp.org/rec/conf/itp/PakK22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}}

@BOOK{Luenberger:1969,
 AUTHOR = {Luenberger, David G.},
 TITLE = {Optimization by Vector Space Methods},
 YEAR = {1969},
 PUBLISHER = {John Wiley and Sons}}

@BOOK{CheneyKincaid:2009,
 AUTHOR = {Cheney, Ward and Kincaid, David},
 TITLE = {Linear Algebra: Theory and Applications},
 YEAR = {2009},
 PUBLISHER = {Jones and Bartlett publishers}}

@article{Gonda:2004,
author={Gonda, Eikou and Miyata, Hitoshi and Ohkita, Masaaki},
title={Self-Turning of Fuzzy Rules with Different Types of {MSF}s (in {J}apanese)},
journal={Journal of Japan Society for Fuzzy Theory and Intelligent Informatics},
ISSN={13477986},
year={2004},
volume={16},
number={6},
pages={540--550},
DOI={10.3156/jsoft.16.540},
URL={https://cir.nii.ac.jp/crid/1390001205185848192}}

@article{Giachetti:1997,
title = {A parametric representation of fuzzy numbers and their arithmetic operators},
journal = {Fuzzy Sets and Systems},
volume = {91},
number = {2},
pages = {185--202},
year = {1997},
issn = {0165-0114},
doi = {10.1016/S0165-0114(97)00140-1},
url = {https://www.sciencedirect.com/science/article/pii/S0165011497001401},
author = {Giachetti, Ronald E. and Young, Robert E.}}

@inproceedings{Luciano:2009,
  title={Fuzzy Arithmetic with Parametric {LR} Fuzzy Numbers},
  author={Stefanini, Luciano and Sorini, Laerte},
  booktitle={Proceedings of the Joint 2009 International Fuzzy Systems Association
    World Congress and 2009 European Society of Fuzzy Logic and Technology Conference},
  pages={600--605},
  year={2009}}
  
@article{RudnickiComm:2001,
  author    = {Rudnicki, Piotr and
               Schwarzweller, Christoph and
               Trybulec, Andrzej},
  title     = {Commutative Algebra in the {M}izar System},
  journal   = {Journal of Symbolic Computation},
  volume    = {32},
  number    = {1/2},
  year      = {2001},
  pages     = {143--169},
  doi       = {10.1006/jsco.2001.0456},
  url       = {http://dx.doi.org/10.1006/jsco.2001.0456}}
 
@BOOK{Fulton69,
 AUTHOR={Fulton, William},
 TITLE={{A}lgebraic Curves. {A}n Introduction to Algebraic Geometry},
 PUBLISHER={The Benjamin/Cummings Publishing Company},
 YEAR={1969}}

@BOOK{Stichtenoth08,
 AUTHOR={Stichtenoth, Henning},
 TITLE={Algebraic Function Fields and Codes},
 PUBLISHER={Springer},
 YEAR={2008}}

@book{kurosh:1955,
  title={The Theory of Groups},
  author={Kurosh, Aleksandr Gennadievich},
  volume={1},
  year={1955},
  publisher={Chelsea Publishing Company}}

@book{aschbacher2000finite,
  title={Finite Group Theory},
  author={Aschbacher, Michael},
  volume={10},
  year={2000},
  publisher={Cambridge University Press}}

@BOOK{Apostol:1967,
 AUTHOR = {Apostol, Tom M.},
 TITLE = {Calculus},
 PUBLISHER = {John Wiley \& Sons},
 YEAR = {1967},
 VOLUME = {I},
 EDITION = {Second}}

@BOOK{Courant:1988,
 AUTHOR = {Courant, Richard and McShane, Edward James},
 TITLE = {Differential and Integral Calculus},
 PUBLISHER = {John Wiley \& Sons},
 YEAR = {1988}}

@article{Boldo:2015,
  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},
  year={2015},
  volume={26},
  pages={1196--1233},
  url={https://api.semanticscholar.org/CorpusID:13018804}}

@inproceedings{Boldo:2012,
  author       = {Boldo, Sylvie and
                  Lelay, Catherine and
                  Melquiond, Guillaume},
  editor       = {Chris Hawblitzel and Dale Miller},
  title        = {Improving Real Analysis in {C}oq: A User-Friendly Approach to Integrals
                  and Derivatives},
  booktitle    = {Certified Programs and Proofs -- Second International Conference, {CPP}
                  2012, Kyoto, Japan, December 13--15, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7679},
  pages        = {289--304},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-35308-6\_22},
  doi          = {10.1007/978-3-642-35308-6\_22}}

@Inbook{Gamboa:2000,
author={Gamboa, Ruben},
editor={Kaufmann, Matt and Manolios, Panagiotis and Moore, J. Strother},
title={Continuity and Differentiability},
bookTitle={Computer-Aided Reasoning: ACL2 Case Studies},
year={2000},
publisher={Springer US},
pages={301--315},
isbn={978-1-4757-3188-0},
doi={10.1007/978-1-4757-3188-0_18}}

@InProceedings{Fleuriot:2000,
author="Fleuriot, Jacques D.",
editor="Aagaard, Mark and Harrison, John",
title="On the Mechanization of Real Analysis in {I}sabelle/{HOL}",
booktitle="Theorem Proving in Higher Order Logics",
year="2000",
publisher="Springer Berlin Heidelberg",
pages="145--161",
isbn="978-3-540-44659-0"}

@InProceedings{LeeRudnicki:2007,
author="Lee, Gilbert and Rudnicki, Piotr",
editor="Kauers, Manuel and Kerber, Manfred and Miner, Robert and Windsteiger, Wolfgang",
title="Alternative Aggregates in {M}izar",
booktitle="Towards Mechanized Mathematical Assistants",
year="2007",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="327--341",
isbn="978-3-540-73086-6",
doi = "10.1007/978-3-540-73086-6_26"}

@inproceedings{Thiemann:2016,
author = {Thiemann, Ren\'{e} and Yamada, Akihisa},
title = {Formalizing {J}ordan {N}ormal {F}orms in {I}sabelle/{HOL}},
year = {2016},
isbn = {9781450341271},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/2854065.2854073},
booktitle = {Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs},
pages = {88--99}}

@article{Noschinski:2015,
  author       = {Noschinski, Lars},
  title        = {A Graph Library for {I}sabelle},
  journal      = {Mathematics in Computer Science},
  volume       = {9},
  number       = {1},
  pages        = {23--39},
  year         = {2015},
  doi          = {10.1007/s11786-014-0183-z}}

@techreport{Butler:1998,
author = {Butler, Ricky W. and Sjogren, Jon A.},
year = {1998},
institution = {NASA Langley},
title = {A {PVS} Graph Theory Library}}

@inproceedings{Chou:1994,
  author       = {Chou, Ching{-}Tsun},
  editor       = {Thomas F. Melham and
                  Juanito Camilleri},
  title        = {A Formal Theory of Undirected Graphs in Higher-Order Logic},
  booktitle    = {Higher Order Logic Theorem Proving and Its Applications, 7th International
                  Workshop, Valletta, Malta, September 19--22, 1994, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {859},
  pages        = {144--157},
  publisher    = {Springer},
  year         = {1994},
  doi          = {10.1007/3-540-58450-1\_40}}

@article{Aransay:2017,
  author       = {Jes{\'{u}}s Aransay and Jose Divas{\'{o}}n},
  title        = {A Formalisation in {HOL} of the Fundamental Theorem of Linear Algebra
                  and Its Application to the Solution of the Least Squares Problem},
  journal      = {Journal of Automated Reasoning},
  volume       = {58},
  number       = {4},
  pages        = {509--535},
  year         = {2017},
  doi          = {10.1007/s10817-016-9379-z}}

@inproceedings{Naumowicz:2023,
  author       = {Naumowicz, Adam},
  editor       = {Catherine Dubois and Manfred Kerber},
  title        = {Extending Numeric Automation for Number Theory Formalizations in {M}izar},
  booktitle    = {Intelligent Computer Mathematics -- 16th International Conference,
                  {CICM} 2023, Cambridge, UK, September 5--8, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14101},
  pages        = {309--314},
  publisher    = {Springer},
  year         = {2023},
  doi          = {10.1007/978-3-031-42753-4\_23}}

@article{Ehrlich,
  author    = {Ehrlich, Philp},
  title     = {Number Systems with Simplicity Hierarchies: {A} Generalization of
               {C}onway's Theory of Surreal Numbers},
  journal   = {Journal of Symbolic Logic},
  volume    = {66},
  number    = {3},
  pages     = {1231--1258},
  year      = {2001},
  url       = {https://doi.org/10.2307/2695104},
  doi       = {10.2307/2695104}}

@article{Ehrlich2011,
  author    = {Ehrlich, Philip},
  title     = {Conway names, the simplicity hierarchy and the surreal number tree},
  journal   = {Journal of Logic and Analysis},
  volume    = {3},
  number    = {1},
  pages     = {1--26},
  year      = {2011},
  doi       = {10.4115/jla.2011.3.1}}

@ARTICLE{Ehrlich2012,
  AUTHOR =       {Ehrlich, Philip},
  TITLE =        {The absolute arithmetic continuum and the unification of all numbers great and small},
  JOURNAL =      {The Bulletin of Symbolic Logic},
  YEAR =         {2012},
  volume =       {18},
  number =       {1},
  pages =        {1--45},
  doi = {10.2178/bsl/1327328438}}

@article{Dybjer00,
  author    = {Dybjer, Peter},
  title     = {A General Formulation of Simultaneous Inductive-Recursive Definitions
               in Type Theory},
  journal   = {The Journal of Symbolic Logic},
  volume    = {65},
  number    = {2},
  pages     = {525--549},
  year      = {2000},
  url       = {https://doi.org/10.2307/2586554},
  doi       = {10.2307/2586554}}


@inproceedings{holzf,
  author    = {Obua, Steven},
  title     = {Partizan Games in {I}sabelle/{HOLZF}},
  booktitle = {Theoretical Aspects of Computing -- {ICTAC} 2006},
  pages     = {272--286},
  year      = {2006},
  editor    = {Kamel Barkaoui and
               Ana Cavalcanti and
               Antonio Cerone},
  series    = {LNCS},
  volume    = {4281},
  publisher = {Springer}}

@inproceedings{Mamane04,
  author    = {Mamane, Lionel Elie},
  editor    = {Jean{-}Christophe Filli{\^{a}}tre and
               Christine Paulin{-}Mohring and
               Benjamin Werner},
  title     = {Surreal Numbers in {C}oq},
  booktitle = {Types for Proofs and Programs, {TYPES} 2004},
  series    = {LNCS},
  volume    = {3839},
  pages     = {170--185},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/11617990\_11},
  doi       = {10.1007/11617990\_11}}

@article{schleicher,
author = {Schleicher, Dierk and Stoll, Michael},
year = {2006},
title = {An Introduction to {C}onway's Games and Numbers},
volume = {6},
pages = {359--388},
journal = {Moscow Mathematical Journal},
doi = {10.17323/1609-4514-2006-6-2-359-388}}

@Article{alabdullah,
  author =       {Alabdullah, Maan T. and El-Seidy, Essam and Morcos, Neveen S.},
  title =        {On Numbers and Games},
  journal =      {International Journal of Scientific and Engineering Research},
  year =         {2020},
  pages     = {510--517},
  volume =       {11},
  month =        {February}}

@BOOK{Alling,
  AUTHOR =       {Alling, Norman L.},
  TITLE =        {Foundations of Analysis Over Surreal Number Fields},
  PUBLISHER =    {North-Holland},
  YEAR =         {1987},
  isbn={9780444702265},
  lccn={87006735},
   number={141},
  series={Annals of Discrete Mathematics}}

@BOOK{Gat11,
      AUTHOR = {Gathmann, Andreas},
      TITLE = {Einf\"{u}hrung in die Algebra},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {2011}}

@article{DuboisPrade:1978,
 AUTHOR={Dubois, Didier and Prade, Henri},
 TITLE={Operations on fuzzy numbers},
journal = {International Journal of Systems Science},
volume = {9},
number = {6},
pages = {613--626},
year  = {1978},
publisher = {Taylor and Francis},
doi = {10.1080/00207727808941724}}

@INPROCEEDINGS{Mitsuishi:2016,
  author={Mitsuishi, Takashi and Terashima, Takanori and  Shimada, Nami and Homma, Toshimichi and Shidama, Yasunari},
  booktitle={2016 IEEE Symposium on Sensorless Control for Electrical Drives (SLED)},
  title={Approximate reasoning using {LR} fuzzy number as input for sensorless fuzzy control},
  year={2016},
  pages={1--5},
  doi={10.1109/SLED.2016.7518804}}

@BOOK{Apostol:1969II,
 AUTHOR = {Apostol, Tom M.},
 TITLE = {Calculus},
 PUBLISHER = {Wiley},
 YEAR = {1969},
 VOLUME = {II},
 EDITION = {Second}}

@inproceedings{GrabowskiMitsuishiLat:2015,
Author = {Grabowski, Adam and Mitsuishi, Takashi},
Editor = {Ciucci, D. and Wang, G. and Mitra, S. and Wu, W.Z.},
Title = {Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets},
Booktitle = {Rough Sets and Knowledge Technology --
 10th International Conference held as part of the International Joint Conference on Rough Sets
   (IJCRS), Tianjin, PR China, November 20--23, 2015, Proceedings},
Series = {Lecture Notes in Artificial Intelligence},
Year = {2015},
Volume = {9436},
Pages = {347--356},
DOI = {10.1007/978-3-319-25754-9\_31},
  publisher = {Springer}}

@article{Drewniak:2006,
 AUTHOR = {Drewniak, J\'{o}zef},
 TITLE = {Invariant fuzzy implications},
 JOURNAL = {Soft Computing},
 VOLUME = {10},
 PAGES = {506--513},
 YEAR  = {2006}}

@BOOK{Smith:1958,
 AUTHOR = {Smith, Edward Staples and Meyer, Salkover and Justice, Howard K.},
 TITLE = {Calculus},
 PUBLISHER = {John Wiley and Sons},
 YEAR = {1958},
 EDITION = {Second}}

@BOOK{Lang:2012,
 AUTHOR = {Lang, Serge},
 TITLE = {Calculus of Several Variables},
 PUBLISHER = {Springer},
 YEAR = {2012},
 EDITION = {Third}}

@article{Kaprekar:1955,
 AUTHOR = {Kaprekar, D. R.},
 TITLE = {Multidigital Numbers},
 JOURNAL = {Scripta Mathematica},
 VOLUME = {21},
 PAGES = {27},
 YEAR = {1955}}

@article{Nutshell:2010,
 AUTHOR = {Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
 TITLE = {Mizar in a Nutshell},
 JOURNAL = {Journal of Formalized Reasoning},
 VOLUME = {3},
 NUMBER = {2},
 YEAR = {2010},
 PAGES = {153--245}}

@BOOK{Dickson:1952,
 AUTHOR = {Dickson, Leonard Eugene},
 TITLE = {History of Theory of Numbers},
 PUBLISHER = {New York},
 YEAR = {1952}}

@article{Nguyen:2022,
author = {Nguyen Xuan Tho},
title = {On a remark of {S}ierpi{\'n}ski},
volume = {52},
journal = {Rocky Mountain Journal of Mathematics},
number = {2},
publisher = {Rocky Mountain Mathematics Consortium},
pages = {717--726},
year = {2022},
doi = {10.1216/rmj.2022.52.717}}

@article{IsaGeoCoq:2021,
  author  = {Coghetto, Roland},
  title   = {Tarski's Parallel Postulate implies the 5th {P}ostulate of {E}uclid, the {P}ostulate of {P}layfair and the Original {P}arallel {P}ostulate of {E}uclid},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/IsaGeoCoq.html},
             Formal proof development},
  ISSN    = {2150-914x}}


@book{Bertot04Coq,
author = {Bertot, Yves and Casteran, Pierre},
title = {Interactive Theorem Proving and Program Development},
year = {2004},
isbn = {3540208542},
publisher = {Springer}}


@inproceedings{Bertot08Coq,
  author    = {Bertot, Yves},
  title     = {A Short Presentation of {C}oq},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2008)},
  pages     = {12--16},
  year      = {2008},
  editor    = {Otmane A{\"{\i}}t Mohamed and
               C{\'{e}}sar A. Mu{\~{n}}oz and
               Sofi{\`{e}}ne Tahar},
  series    = {LNCS},
  volume    = {5170},
  publisher = {Springer},
  doi = {10.1007/978-3-540-71067-7_3}}


@book{IsabelleHOLNPW,
  author = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
  title = {Isabelle/{HOL} -- A Proof Assistant for {H}igher-{O}rder {L}ogic},
  isbn = {3-540-43376-7},
  publisher = {Springer},
  series = {LNCS},
  volume = {2283},
  year = {2002}}

@book{IsabelleHOLNG,
author = {Nipkow, Tobias and Klein, Gerwin},
title = {Concrete Semantics: With {I}sabelle/{HOL}},
year = {2014},
publisher = {Springer}}

@InProceedings{IsabelleMLT,
author={Wenzel, Makarius and Paulson, Lawrence C. and Nipkow, Tobias},
editor={Mohamed, Otmane Ait and Mu{\~{n}}oz, C{\'e}sar and Tahar, Sofi{\`e}ne},
title={The {I}sabelle Framework},
booktitle={Theorem Proving in Higher Order Logics},
year={2008},
publisher={Springer Berlin Heidelberg},
pages={33--38}}

@inproceedings{CNFPakKaliszyk24,
  author       = {P\k{a}k, Karol and Kaliszyk, Cezary},
  editor       = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  title        = {Conway Normal Form: Bridging Approaches for Comprehensive Formalization
                  of Surreal Numbers},
  booktitle    = {15th International Conference on Interactive Theorem Proving, {ITP}
                  2024, {S}eptember 9-14, 2024, {T}bilisi, {G}eorgia},
  series       = {LIPIcs},
  volume       = {309},
  pages        = {29:1--29:18},
  publisher    = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2024},
  doi          = {10.4230/LIPICS.ITP.2024.29}}

@book{Carmichael:1915,
author = {Carmichael, Robert D.},
title = {Diophantine Analysis},
year = {1915},
publisher = {New York, John Wiley \& Sons}}

@book{BarbeauPell:2003,
author = {Barbeau, Edward J.},
title = {Pell's Equation},
series = {Problem Books in Mathematics},
year = {2003},
publisher = {Springer}}

@article{SchinzelCM:1959,
author = {Schinzel, Andrzej},
journal = {Compositio Mathematica},
pages = {74--76},
title = {D{\'e}monstration d'une cons{\'e}quence de l'hypoth{\`e}se de {G}oldbach},
url = {https://eudml.org/doc/88862},
volume = {14},
year = {1959}}

@article{SchinzelSierp:1958,
author = {Schinzel, Andrzej and Sierpi\'nski, Wac{\l}aw},
journal = {Acta Arithmetica},
number = {3},
pages = {185--208},
title = {Sur certaines hypoth{\`e}ses concernant les nombres premiers},
url = {https://eudml.org/doc/206115},
volume = {4},
year = {1958}}

@article{SierpinskiAA:1961, 
title={Remarques sur le travail de {M. J. W. S.} {C}assels <<{O}n a diophantine equation>>}, 
volume={6}, 
number={4}, 
journal={Acta Arithmetica}, 
author={Sierpi\'nski, Wac{\l}aw}, 
url = {https://eudml.org/doc/206729},
year={1961}, 
pages={469--471}}

@article{Hurwitz:1893,
author = {Hurwitz, Adolf},
journal = {Mathematische Annalen},
pages = {220--221},
title = {Beweis der {T}ranscendenz der {Z}ahl e},
url = {https://eudml.org/doc/157680},
volume = {43},
year = {1893}}

@book{KnuthSurreal:1974,
author = {Knuth, Donald E.},
title = {Surreal Numbers: How Two Ex-students Turned on to Pure Mathematics and Found Total Happiness},
year = {1974},
publisher = {Addison-Wesley}}

@article{SierpinskiMath:1956, 
title={Sur les d{\'e}compositions de nombres rationells en fractions primaires}, 
volume={65}, 
journal={Mathesis}, 
author={Sierpi\'nski, Wac{\l}aw}, 
year={1956}, 
pages={16--32}}

@book{MordellDE:1969,
author = {Mordell, Louis J.},
title = {Diophantine Equations},
year = {1969},
publisher = {Academic Press}}

@BOOK{NirL:1961,
 AUTHOR = {Nirenberg, Louis},
 TITLE = {Functional Analysis: Lectures Given in 1960--61. {N}otes by {L}esley {S}ibner},
 YEAR = {1961},
 PUBLISHER = {New York University}}

@BOOK{Kashiwara:2006,
 AUTHOR = {Kashiwara, Masaki and Schapira, Pierre},
 TITLE = {Categories and Sheaves},
  SERIES = {Grundlehren der Mathematischen Wissenschaften},
  VOLUME = {332},
DOI = {10.1007/3-540-27950-4},
 YEAR = {2006},
 PUBLISHER = {Springer}}

@BOOK{Fujiwara:1929,
    AUTHOR = {Fujiwara, Matsusaburo},
     TITLE = {Algebra vol 2, Japanese},
 PUBLISHER = {Uchida Rokakuho Publishing Co., Ltd},
  edition = {1st},
      YEAR = 1929}

@BOOK{DicksonII:1920,
 AUTHOR = {Dickson, Leonard Eugene},
 TITLE = {History of Theory of Numbers, Volume {II}; Diophantine Analysis},
 PUBLISHER = {Carnegie Institution},
 YEAR = {1920}}

@article{Moessner:1936, 
title = {General Formulae for Constructing and Solving certain Simultaneous Equations}, 
volume = {3}, 
journal = {The Mathematics Student}, 
author = {Moessner, Alfred}, 
year = {1936}}

@BOOK{Leinster:2014,
 AUTHOR = {Leinster, Tom},
 TITLE = {Basic Category Theory},
 PUBLISHER = {Cambridge University Press},
 YEAR = {2014}}

@BOOK{Baker:1990,
 AUTHOR = {Baker, Alan},
 TITLE = {Transcendental Number Theory},
 PUBLISHER = {Cambridge University Press},
 YEAR = {1990}}

@BOOK{Lang:1966,
 AUTHOR = {Lang, Serge},
 TITLE = {Introduction to Transcendental Numbers},
 PUBLISHER = {Addison-Wesley Pub. Co.},
 YEAR = {1966}}

@article{Eberl:2017,
  author  = {Eberl, Manuel},
  title   = {The Transcendence of $e$},
  journal = {Archive of Formal Proofs},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/E_Transcendental.html},
             Formal proof development},
  ISSN    = {2150-914x}}

@article{PeterLax:1995,
    author = {Lax, Peter David},
    title = {A Short Path to the Shortest Path},
    journal = {The American Mathematical Monthly},
    volume = {102},
    number = {2},
    pages = {158--159},
    year  = {1995},
    publisher = {Taylor \& Francis}}

@article{Hehl:2013,
  title={The Isoperimetric Inequality},
  author={Hehl, Andreas},
  journal={Proseminar Curves and Surfaces, Universitaet Tuebingen, Tuebingen},
  year={2013}}

@article{Viktor:2005,
    author = {Bl{\aa}sj{\"o}, Viktor},
    title = {The Isoperimetric Problem},
    journal = {The American Mathematical Monthly},
    volume = {112},
    number = {6},
    pages = {526--566},
    year  = {2005},
    publisher = {Taylor \& Francis}}

@book{Hermite:1874,
author = {Hermite, Charles},
location = {Paris},
publisher = {Gauthier-Villars},
title = {Sur la fonction exponentielle},
   NOTE = {\href{http://eudml.org/doc/203956}{\tt http://eudml.org/doc/203956}},
url = {http://eudml.org/doc/203956},
year = {1874}}

@book{Pressley:2010,
  title={Elementary Differential Geometry},
  author={Pressley, Andrew N.},
  year={2010},
  publisher={Springer Science \& Business Media}}

@book{Metamath:2019,
      author = {Megill, Norman D. and Wheeler, David A.},
      title = {Metamath: A Computer Language for Mathematical Proofs},
      year = {2019},
      publisher = {Lulu Press},
      address = {Morrisville, North Carolina},
   NOTE = {\href{http://us.metamath.org/downloads/metamath.pdf}{\tt http://us.metamath.org/downloads/metamath.pdf}},
      url = {http://us.metamath.org/downloads/metamath.pdf}}

@inproceedings{Lean4:2021,
author = {Moura, Leonardo de and Ullrich, Sebastian},
title = {The {L}ean 4 Theorem Prover and Programming Language},
year = {2021},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
url = {https://doi.org/10.1007/978-3-030-79876-5_37},
doi = {10.1007/978-3-030-79876-5_37},
booktitle = {Automated Deduction -- CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12--15, 2021, Proceedings},
pages = {625--635}}

@BOOK{Isaacs:2009,
      AUTHOR = {Isaacs, I.~Martin},
      TITLE = {Algebra, {A} {G}raduate {C}ourse},
      PUBLISHER = {American Mathematical Society},
      YEAR = {2009}}

@BOOK{Christmann:1989,
      AUTHOR = {Christmann, Norbert},
      TITLE = {Einf\"{u}hrung in die (lineare) {A}lgebra},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1989}}

@Article{Bes:1997,
  author    = {B{\'e}s, Alexis},
  journal   = {Annals of Pure and Applied Logic},
  title     = {On {P}ascal Triangles Modulo a Prime Power},
  year      = {1997},
  issn      = {0168-0072},
  number    = {1},
  pages     = {17--35},
  volume    = {89},
  doi       = {10.1016/s0168-0072(97)85376-6},
  publisher = {Elsevier BV}}

@InProceedings{granville1997arithmetic,
  author       = {Granville, Andrew},
  booktitle    = {Organic Mathematics: Proceedings of the Organic Mathematics Workshop},
  title        = {Arithmetic properties of binomial coefficients. {I}. {B}inomial coefficients modulo prime powers},
  year         = {1997},
  address      = {Burnaby, BC},
  editor       = {Jonathan M. Borwein},
  organization = {American Mathematical Soc.},
  pages        = {253--276},
  series       = {CMS conference proceedings},
  volume       = {20},
  isbn         = {9780821806685},
  lccn         = {97000179},
  url          = {https://books.google.pl/books?id=bEgtaaU0QRoC}}

@Article{Anggoro:2010,
  author    = {Anggoro, Alif and Liu, Eddy and Tulloch, Angus},
  journal   = {The College Mathematics Journal},
  title     = {The {R}ascal Triangle},
  year      = {2010},
  issn      = {1931-1346},
  number    = {5},
  pages     = {393--395},
  volume    = {41},
  doi       = {10.4169/074683410x521991},
  publisher = {Informa UK Limited}}

@Article{Lapis:2012,
  author       = {Lapis, W{\l}odzimierz},
  journal      = {Investigationes Linguisticae},
  title        = {Dystynktywno{\'s}{\'c} ci\k{a}g{\'o}w},
  year         = {2012},
  pages        = {58--71},
  volume       = {25},
  doi          = {10.14746/il.2012.25.4},
  url          = {https://pressto.amu.edu.pl/index.php/il/article/view/9760}}

@inproceedings{BoldoCPP:2017,
author = {Boldo, Sylvie and Cl\'{e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
title = {A {C}oq formal proof of the {L}ax-{M}ilgram theorem},
year = {2017},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3018610.3018625},
doi = {10.1145/3018610.3018625},
booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
pages = {79–-89},
location = {Paris, France},
series = {CPP 2017}}

@article{Li:2024,
      title={Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization}, 
      author={Li, Chenyi and Wang, Ziyu and He, Wanyi and Wu, Yuxuan and Xu, Shengyang and Wen, Zaiwen},
      year={2024},
      journal = {arXiv preprint arXiv:2403.11437},
      eprint={2403.11437},
      archivePrefix={arXiv},
      primaryClass={math.OC},
      url={https://arxiv.org/abs/2403.11437}}

@InProceedings{Rothgang:2021,
author="Rothgang, Colin
and Korni{\l}owicz, Artur
and Rabe, Florian",
editor="Kamareddine, Fairouz
and Sacerdoti Coen, Claudio",
title="A New Export of the {M}izar {M}athematical {L}ibrary",
booktitle="Intelligent Computer Mathematics",
year="2021",
publisher="Springer International Publishing",
address="Cham",
doi = "10.1007/978-3-030-81097-9_17",
pages="205--210"}

@article{Ascoli:1883,
    author = {Ascoli, Giulio},
    title = {Le curve limite di una variet\`{a} data di curve},
    journal = {Atti della R. Accad. Dei Lincei Memorie della Cl. Sci. Fis. Mat. Nat.},
    volume = {18},
    number = {3},
    pages = {521--586},
    year  = {1883--1884}}

@article{Arzela:1895,
    author = {Arzel\`{a}, Cesare},
    title = {Sulle funzioni di linee},
    journal = {Mem. Accad. Sci. Ist. Bologna Cl. Sci. Fis. Mat.},
    volume = {5},
    number = {5},
    pages = {55--74},
    year  = {1895}}

@inproceedings{Mathlib:2020,
author = {The mathlib Community},
title = {The {L}ean mathematical library},
year = {2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3372885.3373824},
doi = {10.1145/3372885.3373824},
booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {367--381},
location = {New Orleans, LA, USA},
series = {CPP 2020}}

@article{Chajda:1976,
author = {Chajda, Ivan and Zelinka, Bohdan},
journal = {Czechoslovak Mathematical Journal},
number = {2},
pages = {259--269},
publisher = {Institute of Mathematics, Academy of Sciences of the Czech Republic},
title = {Weakly Associative Lattices and Tolerance Relations},
url = {http://eudml.org/doc/12937},
volume = {26},
year = {1976}}

@article{Osserman:1978,
author = {Osserman, Robert},
journal = {Bulletin of American Mathematical Society},
number = {84},
pages = {1182--1238},
title = {The Isoperimetric Inequality},
volume = {6},
year = {1978}}

@article{Siegel:2003,
title = {An Isoperimetric Theorem in Plane Geometry},
author = {Siegel, Alan},
year = {2003},
doi = {10.1007/s00454-002-2809-1},
volume = {29},
pages = {239--255},
journal = {Discrete and Computational Geometry},
publisher = {Springer, New York},
number = {2}}

@article{Straatsma:2022,
title = {Towards Formalising the Isoperimetric Theorem},
author = {Straatsma, Marten},
journal = {\rm BSc thesis, Radboud University Nijmegen},
url = {https://www.cs.ru.nl/bachelors-theses/2022/Marten_Straatsma___1041007___Towards_Formalising_the_Isoperimetric_Theorem.pdf},
year = {2022}}

@InCollection{HOLLightIso:2023,
author = {Harrison, John},
   TITLE = {The Isoperimetric Inequality},
url = {https://github.com/jrh13/hol-light/blob/master/100/isoperimetric.ml},
year = {2023},
    NOTE = {Available online at {\tt https://github.com/jrh13/hol-light/blob/master/100/isoperimetric.ml}}}

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

@article{Edmonds:2020,
  author  = {Edmonds, Chelsea},
  title   = {Lucas's Theorem},
  journal = {Archive of Formal Proofs},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Lucas_Theorem.html},
             Formal proof development},
  ISSN    = {2150-914x}}

@article{Fine:1947,
author = {Fine, N.J.},
journal = {The American Mathematical Monthly},
number = {10},
pages = {589--592},
title = {Binomial Coefficients Modulo a Prime},
doi = {10.2307/2304500},
volume = {54},
year = {1947}}

@article{Karayel:2022,
  author  = {Karayel, Emin},
  title   = {Finite Fields},
  journal = {Archive of Formal Proofs},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Finite_Fields.html},
             Formal proof development},
  ISSN    = {2150-914x}}

@article{Polya:1918,
  author  = {P{\`o}lya, Georg},
  title   = {Zur arithmetischen {U}ntersuchung der {P}olynome},
  journal = {Mathematische Zeitschrift},
  year    = {1918},
  pages = {142--148},
  volume = {1},
  number = {1}}

@article{Bertrand:1845,
  author  = {Bertrand, Joseph},
  title   = {M{\'e}moire sur le nombre de valeurs que peut prendre une fonction quand on y permute les lettres qu'elle renferme},
  journal = {Journal de l'{\'E}cole Royale Polytechnique},
  year    = {1845},
  pages = {123--140},
  volume = {18},
  number = {30}}

@article{Chebyshev:1852,
  author  = {Tchebychev, Pafnuty},
  title   = {M{\'e}moire sur les nombres premiers},
  journal = {Journal de math{\'e}matiques pures et appliqu{\'e}es},
  year    = {1852},
  pages = {366--390},
  volume = {1}}

@INPROCEEDINGS{Suszko:1975,
       AUTHOR = {Suszko, Roman},
        TITLE = {Abolition of the {Fregean} axiom},
    BOOKTITLE = {Logic Colloquium: Symposium on Logic held at Boston, 1972--73},
         YEAR = {1975},
       EDITOR = {R.~Parikh},
        PAGES = {169--239},
       SERIES = {Lecture Notes in Mathematics},
       VOLUME = {453},
    PUBLISHER = {Springer},
      ADDRESS = {Heidelberg}}

@article{Edmonds2:2023,
title={Formalising Combinatorial Structures and Proof Techniques in {Isabelle/HOL}},
doi={10.17863/CAM.108886},
journal={\rm Apollo -- University of Cambridge Repository},
author = {Edmonds, Chelsea},
year = {2023}}

@article{Smoluk:2017,
author={Smoluk, Antoni},
journal={Didactics of Mathematics},
title={Statystyka w {XXI} wieku. {P}rzysz{\l}o{\'s}{\'c} statystyki},
year={2017},
issn={2450-1123},
number={18},
pages={59--70},
volume={14},
doi={10.15611/dm.2017.14.06},
publisher={Wroclaw University of Economics and Business}}

@article{Zedam:2023,
title = {Triangular Norms on Bounded Trellises},
journal = {Fuzzy Sets and Systems},
volume = {462},
pages = {108468},
year = {2023},
doi = {10.1016/j.fss.2023.01.003},
url = {https://www.sciencedirect.com/science/article/pii/S0165011423000039},
author = {Zedam, Lemnaouar and {De Baets}, Bernard}}

@article{Skala:1971,
title = {Trellis Theory},
journal = {Algebra Universalis},
volume = {1},
pages = {218--233},
year = {1971},
doi = {10.1007/BF02944982},
author = {Skala, Helen L.}}

@book{Skala:1972,
title = {Trellis Theory},
year = {1972},
bookseries = {Memoirs of the American Mathematical Society, no. 121},
publisher = {Providence, R.I.: American Mathematical Society},
author = {Skala, Helen}}

@article{Yu:2024,
author = {Kong, Yu and Zhao, Bin},
year = {2024},
pages = {108898},
title = {Uninorms on Bounded Trellises},
volume = {481},
journal = {Fuzzy Sets and Systems},
doi = {10.1016/j.fss.2024.108898}}

@article{ROUGHAN2019,
title = {Practically surreal: surreal arithmetic in {J}ulia},
journal = {SoftwareX},
volume = {9},
pages = {293--298},
year = {2019},
issn = {2352-7110},
doi = {https://doi.org/10.1016/j.softx.2019.03.005},
author = {Roughan, Matthew}}

@ARTICLE{NietoParityofdyadic,
  AUTHOR = {Nieto, J. A. and Escalante-Javalera, J. A. and Somera-Patr\'on, C. A. and Villasenor-Gonz\'alez, E. J.},
  TITLE =        {Parity of dyadic rationals and surreal numbers},
  JOURNAL =      {Far East Journal of Mathematical Sciences (FJMS)},
  YEAR =         {2024},
  number =       {2},
  pages =        {155--167},
 DOI = {https://doi.org/10.17654/0972087124010},
  month =        {May}}


@misc{Hatcher:2001,
  TITLE = {Algebraic Topology},
  AUTHOR = {Hatcher, Allen},
  YEAR = {2001},
  PAGES = {XII, 551 p.},
  url={https://pi.math.cornell.edu/~hatcher/AT/AT+.pdf}}

@book{Armstrong:1988,
  title={Groups and Symmetry},
  author={Armstrong, Mark Anthony},
  series={Undergraduate Texts in Mathematics},
  pages={XI, 187 p.},
   NOTE = {\href{https://link.springer.com/book/10.1007/978-1-4757-4034-9}{\tt https://link.springer.com/book/10.1007/978-1-4757-4034-9}},
  url={https://link.springer.com/book/10.1007/978-1-4757-4034-9},
  year={1988},
  publisher={Springer New York}}

@book{Kargapolov:1979,
  title={Fundamentals of the Theory of Groups},
  author={Kargapolov, Mikhail Ivanovich and Merzljakov, Yurii Ivanovich},
  series={Graduate Texts in Mathematics},
  year={1979},
  pages={XVIII, 203 p.},
  publisher={Springer New York},
   NOTE = {\href{https://link.springer.com/book/9781461299660}{\tt https://link.springer.com/book/9781461299660}},
  url={https://link.springer.com/book/9781461299660}}

@book{Robinson:1995,
  title={A Course in the Theory of Groups},
  author={Robinson, Derek J.S.},
  series={Graduate Texts in Mathematics},
  year={1996},
  pages={XVII, 502 p.},
  publisher={Springer New York},
   NOTE = {\href{https://link.springer.com/book/10.1007/978-1-4419-8594-1}{\tt https://link.springer.com/book/10.1007/978-1-4419-8594-1}},
  url={https://link.springer.com/book/10.1007/978-1-4419-8594-1}}