Change language

Wyszukiwarka projektów

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

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ące (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)

  1. 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

  2. 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

  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:
    Opublikowana
    DOI:
    10.1515/forma-2017-0019 – link do publikacji

  4. 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

  5. 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

  6. 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

  7. 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

  8. 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

  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. Grothendieck Universes

    Autorzy:
    Karol Pąk
    Status:
    Przyjęta do publikacji

Teksty w publikacjach pokonferencyjnych (11)

  1. Combining the Syntactic and Semantic Representations of Mizar Proofs

    Autorzy:
    Karol Pąk
    Konferencja:
    Federated Conference on Computer Science, 2018 (rok: 2018, strony: 145-153), Wydawca: Annals of Computer Science and Information Systems, IEEE
    Data:
    konferencja 9-12 wrzesień
    Status:
    Opublikowana

  2. Declarative Proof Translation

    Autorzy:
    Cezary Kaliszyk, Karol Pąk
    Konferencja:
    10th International Conference on Interactive Theorem Proving (ITP 2019) (rok: 2019, strony: 35:1-35:7), Wydawca: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 8-13 września
    Status:
    Opublikowana

  3. 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, strony: 9:1--9:16), Wydawca: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 8-13 września
    Status:
    Opublikowana

  4. 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, strony: 227-236), Wydawca: Annals of Computer Science and Information Systems, IEEE
    Data:
    konferencja 3-6 wrzesień
    Status:
    Opublikowana
    DOI:
    link do publikacji

  5. Isabelle Import Infrastructure for the Mizar Mathematical Library

    Autorzy:
    Cezary Kaliszyk, Karol Pąk
    Konferencja:
    Intelligent Computer Mathematics - 11th International Conference (rok: 2018, strony: 131-146), Wydawca: Lecture Notes in Computer Science
    Data:
    konferencja 13- 17 sierpień
    Status:
    Opublikowana

  6. Mizar Set Comprehension in Isabelle Framework

    Autorzy:
    Karol Pąk
    Konferencja:
    Federated Conference on Computer Science, 2018 (rok: 2018, strony: 23-26), Wydawca: Annals of Computer Science and Information Systems
    Data:
    konferencja 9-12 wrzesień
    Status:
    Opublikowana

  7. 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, strony: 163-178), Wydawca: Lecture Notes in Computer Science, Springer
    Data:
    konferencja 15-17 listopad
    Status:
    Opublikowana

  8. 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, strony: 193-207), Wydawca: Lecture Notes in Computer Science, Springer
    Data:
    konferencja 17-21 lipiec
    Status:
    Opublikowana

  9. A Tale of Two Set Theories

    Autorzy:
    Chad E. Brown, Karol Pak
    Konferencja:
    Intelligent Computer Mathematics - 12th International Conference, CICM 2019 (rok: 2019, strony: 44-60), Wydawca: Springer
    Data:
    konferencja 8-12 lipiec
    Status:
    Opublikowana

  10. 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, strony: 223-226), Wydawca: Annals of Computer Science and Information Systems, IEEE
    Data:
    konferencja 3-6 wrsześnia
    Status:
    Opublikowana
    DOI:
    link do publikacji

  11. 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, strony: 46027), Wydawca: CEUR-WS.org
    Data:
    konferencja 13 sierpień
    Status:
    Opublikowana

« Nowe wyszukiwanie

Projekt graficzny i wykonanie: Jakub Piotrowski