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

Jednostka realizująca:

Uniwersytet w Białymstoku, Wydział Matematyki i 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

Czas trwania projektu: 36 miesięcy

Status projektu: Projekt w realizacji

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.

Dane z raportu końcowego

  • Publikacje w czasopismach (7)
  • Teksty w publikacjach pokonferencyjnych (8)
  1. Semantics of Mizar as an Isabelle Object Logic IF: 1,321
    Autorzy:
    Cezary Kaliszyk, Karol Pąk
    Czasopismo:
    Journal of Automated Reasoning (rok: 2018, tom: bd., strony: 01.01.1939), Wydawca: Springer Netherlands
    Status:
    Opublikowane
    Doi:
    10.1007/s10817-018-9479-z - link do publikacji
  2. 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:
    Opublikowane
    Doi:
    10.1515/forma-2017-0014 - link do publikacji
  3. 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:
    Opublikowane
    Doi:
    10.1515/forma-2017-0019 - link do publikacji
  4. 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:
    Opublikowane
    Doi:
    10.2478/forma-2018-0015 - link do publikacji
  5. The Matiyasevich Theorem. Preliminaries
    Autorzy:
    Karol Pąk
    Czasopismo:
    Formalized Mathematics (rok: 2017, tom: 25(4), strony: 317-325), Wydawca: de Gruyter Open
    Status:
    Przyjęte
    Doi:
    10.1515/forma-2017-0029 - link do publikacji
  6. Diophantine sets. Preliminaries
    Autorzy:
    Karol Pąk
    Czasopismo:
    Formalized Mathematics (rok: 2018, tom: 26(1), strony: 81-90), Wydawca: de Gruyter Open
    Status:
    Przyjęte
    Doi:
    10.2478/forma-2018-0007 - link do publikacji
  7. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar IF: 1,636
    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: 01.09.1932), Wydawca: Springer Netherlands
    Status:
    Przyjęte
    Doi:
    10.1007/s10817-017-9440-6 - link do publikacji
  1. 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:
    Opublikowane
  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:
    Opublikowane
  3. 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:
    Opublikowane
  4. 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:
    Opublikowane
  5. 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:
    Opublikowane
  6. 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:
    Opublikowane
  7. 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:
    Opublikowane
  8. 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:
    Przyjęte