Projects funded by the NCN

Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Isabelle Emulator for Mizar: Environment for Mizar Mathematical Library Reverificationa

2015/19/D/ST6/01473

Keywords:

Mizar Isabelle meta-logic machine translation reverification of the proofs

Descriptors:

  • ST6_4: Formal methods, foundations of computer science, including theoretical computer science, quantum algorithms

Panel:

ST6 - Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems

Host institution :

Uniwersytet w Białymstoku, Instytut Informatyki

woj. podlaskie

Other projects carried out by the institution 

Principal investigator (from the host institution):

dr Karol Pąk 

Number of co-investigators in the project: 4

Call: SONATA 10 - announced on 2015-09-15

Amount awarded: 170 440 PLN

Project start date (Y-m-d): 2016-07-20

Project end date (Y-m-d): 2020-03-19

Project duration:: 44 months (the same as in the proposal)

Project status: Project settled

Project description

Download the project description in a pdf file

Note - project descriptions were prepared by the authors of the applications themselves and placed in the system in an unchanged form.

Equipment purchased [PL]

  1. Laptop (7 000 PLN)

Information in the final report

  • Publication in academic press/journals (10)
  • Articles in post-conference publications (11)
  1. Semantics of Mizar as an Isabelle Object Logic
    Authors:
    Cezary Kaliszyk, Karol Pąk
    Academic press:
    Journal of Automated Reasoning (rok: 2018, tom: bd., strony: 14246), Wydawca: Springer Netherlands
    Status:
    Published
    DOI:
    10.1007/s10817-018-9479-z - link to the publication
  2. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
    Authors:
    Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk
    Academic press:
    Journal of Automated Reasoning (rok: 2018, tom: 61, strony: 11933), Wydawca: Springer Netherlands
    Status:
    Published
    DOI:
    10.1007/s10817-017-9440-6 - link to the publication
  3. Grothendieck Universes
    Authors:
    Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2020, tom: 28(2), strony: 211-215), Wydawca: Sciendo
    Status:
    Accepted for publication
    DOI:
    10.2478/forma-2020-0018 - link to the publication
  4. The Matiyasevich Theorem. Preliminaries
    Authors:
    Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2017, tom: 25(4), strony: 317-325), Wydawca: de Gruyter Open
    Status:
    Published
    DOI:
    10.1515/forma-2017-0029 - link to the publication
  5. Basel Problem
    Authors:
    Karol Pąk, Artur Korniłowicz
    Academic press:
    Formalized Mathematics (rok: 2017, tom: 25(2), strony: 149-155), Wydawca: de Gruyter Open
    Status:
    Published
    DOI:
    10.1515/forma-2017-0014 - link to the publication
  6. Basic Diophantine Relations
    Authors:
    Marcin Acewicz, Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2018, tom: 26(2), strony: 175-181), Wydawca: de Gruyter Open
    Status:
    Published
    DOI:
    10.2478/forma-2018-0015 - link to the publication
  7. Pell's Equation
    Authors:
    Marcin Acewicz, Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2017, tom: 25(3), strony: 197-204), Wydawca: de Gruyter Open
    Status:
    Published
    DOI:
    10.1515/forma-2017-0019 - link to the publication
  8. AIM Loops and the AIM Conjecture
    Authors:
    Chad E. Brown, Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2019, tom: 27(4), strony: 321-335), Wydawca: de Gruyter Open
    Status:
    Published
    DOI:
    10.2478/forma-2019-0027 - link to the publication
  9. Diophantine sets. Preliminaries
    Authors:
    Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2018, tom: 26(1), strony: 81-90), Wydawca: de Gruyter Open
    Status:
    Published
    DOI:
    10.2478/forma-2018-0007 - link to the publication
  10. Formalization of the MRDP Theorem in the Mizar System
    Authors:
    Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2019, tom: 27(2), strony: 209-221), Wydawca: de Gruyter Open
    Status:
    Published
    DOI:
    10.2478/forma-2019-0020 - link to the publication
  1. Declarative Proof Translation
    Authors:
    Cezary Kaliszyk, Karol Pąk
    Conference:
    10th International Conference on Interactive Theorem Proving (ITP 2019) (rok: 2019, ), Wydawca: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 8-13 września
    Status:
    Published
  2. Mizar Set Comprehension in Isabelle Framework
    Authors:
    Karol Pąk
    Conference:
    Federated Conference on Computer Science, 2018 (rok: 2018, ), Wydawca: Annals of Computer Science and Information Systems
    Data:
    konferencja 9-12 wrzesień
    Status:
    Published
  3. Progress in the Formalization of Matiyasevich's theorem in the Mizar system
    Authors:
    Karol Pąk
    Conference:
    FMM 2018 - Third workshop on Formal Mathematics for Mathematicians (rok: 2018, ), Wydawca: CEUR-WS.org
    Data:
    konferencja 13 sierpień
    Status:
    Published
  4. Combining the Syntactic and Semantic Representations of Mizar Proofs
    Authors:
    Karol Pąk
    Conference:
    Federated Conference on Computer Science, 2018 (rok: 2018, ), Wydawca: Annals of Computer Science and Information Systems, IEEE
    Data:
    konferencja 9-12 wrzesień
    Status:
    Published
  5. Formalization of Pell's Equations in the Mizar System
    Authors:
    Marcin Acewicz and Karol Pąk
    Conference:
    Federated Conference on Computer Science and Information Systems (rok: 2017, ), Wydawca: Annals of Computer Science and Information Systems, IEEE
    Data:
    konferencja 3-6 wrsześnia
    Status:
    Published
    DOI:
    link to the publication
  6. Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
    Authors:
    Cezary Kaliszyk, Karol Pąk
    Conference:
    Intelligent Computer Mathematics - 10th International Conference (rok: 2017, ), Wydawca: Lecture Notes in Computer Science, Springer
    Data:
    konferencja 17-21 lipiec
    Status:
    Published
  7. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof
    Authors:
    Chad E. Brown, Cezary Kaliszyk, Karol Pąk
    Conference:
    10th International Conference on Interactive Theorem Proving (ITP 2019) (rok: 2019, ), Wydawca: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 8-13 września
    Status:
    Published
  8. A Tale of Two Set Theories
    Authors:
    Chad E. Brown, Karol Pak
    Conference:
    Intelligent Computer Mathematics - 12th International Conference, CICM 2019 (rok: 2019, ), Wydawca: Springer
    Data:
    konferencja 8-12 lipiec
    Status:
    Published
  9. Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
    Authors:
    Cezary Kaliszyk, Karol Pąk
    Conference:
    Mathematical Aspects of Computer and Information Sciences (rok: 2017, ), Wydawca: Lecture Notes in Computer Science, Springer
    Data:
    konferencja 15-17 listopad
    Status:
    Published
  10. Isabelle Import Infrastructure for the Mizar Mathematical Library
    Authors:
    Cezary Kaliszyk, Karol Pąk
    Conference:
    Intelligent Computer Mathematics - 11th International Conference (rok: 2018, ), Wydawca: Lecture Notes in Computer Science
    Data:
    konferencja 13- 17 sierpień
    Status:
    Published
  11. Progress in the Independent Certification of Mizar Mathematical Library in Isabelle
    Authors:
    Cezary Kaliszyk, Karol Pąk
    Conference:
    Federated Conference on Computer Science and Information Systems (rok: 2017, ), Wydawca: Annals of Computer Science and Information Systems, IEEE
    Data:
    konferencja 3-6 wrzesień
    Status:
    Published
    DOI:
    link to the publication

O Narodowym Centrum Nauki

Finansowanie nauki

Współpraca zagraniczna

Centrum prasowe

Deklaracja dostępności
Przetwarzanie danych osobowych
Polityka cookies

Partnerzy