Projekty finansowane przez NCN

Dane kierownika projektu i jednostki realizującej

Szczegółowe informacje o projekcie i konkursie

Słowa kluczowe

Aparatura

Wyczyść formularz

Emulator środowiska systemu Mizar w systemie Isabelle jako narzędzie umożliwiające niezależną weryfikację bazy MML

2015/19/D/ST6/01473

Słowa kluczowe:

Mizar Isabelle metalogika tłumaczenie maszynowe niezależne certyfikowanie dowodów

Deskryptory:

  • ST6_4: Metody formalne, teoretyczne podstawy informatyki w tym informatyka teoretyczna

Panel:

ST6 - Informatyka i technologie informacyjne: technologie i systemy informacyjne, informatyka, obliczenia naukowe, systemy inteligentne

Jednostka realizująca:

Uniwersytet w Białymstoku, Instytut Informatyki

woj. podlaskie

Inne projekty tej jednostki 

Kierownik projektu (z jednostki realizującej):

dr Karol Pąk 

Liczba wykonawców projektu: 4

Konkurs: SONATA 10 - ogłoszony 2015-09-15

Przyznana kwota: 170 440 PLN

Rozpoczęcie projektu: 2016-07-20

Zakończenie projektu: 2020-03-19

Planowany czas trwania projektu: 44 miesięcy (z wniosku)

Status projektu: Projekt rozliczony

Opis Projektu

Pobierz opis projektu w formacie .pdf

Uwaga - opisy projektów zostały sporządzone przez samych autorów wniosków i w niezmienionej formie umieszczone w systemie.

Zakupiona aparatura

  1. Laptop. Za kwotę 7 000 PLN

Dane z raportu końcowego/rocznego

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

O Narodowym Centrum Nauki

Finansowanie nauki

Współpraca zagraniczna

Centrum prasowe

Deklaracja dostępności
Przetwarzanie danych osobowych
Polityka cookies

Partnerzy