Algorithms concerning the legibility of natural deduction proofs

2012/07/N/ST6/02147

Keywords

Descriptors

  • ST6_4: Metody formalne, teoretyczne podstawy informatyki w tym informatyka teoretyczna
  • ST6_6: Algorytmika, algorytmy równoległe, rozproszone i sieciowe, algorytmiczna teoria gier

Panel

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

Host institution

Uniwersytet w Białymstoku, Wydział Matematyki i Informatyki

Voivodeship: 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: 2

Call

PRELUDIUM 4 – announced on 2012-09-15

Amount awarded
98 340 PLN
Project start date
2013-07-08
Project end date
2017-01-07
Project duration
42 months (the same as in the proposal)
Project status
Project settled

Equipment purchased [PL]

  1. Laptop min. czterordzeniowy, dodatkowy monitor.. Cost: 5 000 PLN

Information in the final report

Publication in academic press/journals (8)

  1. Leibniz Series for PI

    Authors:
    Karol Pąk
    Academic press:
    Formalized Mathematics (year: 2016, volume: 24, pages: 275–280), Publisher: Uniwersytet w Białymstoku
    Status:
    Published
    DOI:
    10.1515/forma-2016-0023 – link to the publication
  2. Flexary Operations

    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (year: 2015, volume: 32(2), pages: 81-92), Publisher: University of Białystok
    Status:
    Published
    DOI:
    10.1515/forma-2015-0008 – link to the publication
  3. Euler's Partition Theorem

    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (year: 2015, volume: 23(2), pages: 93-99), Publisher: University of Białystok
    Status:
    Published
    DOI:
    10.1515/forma-2015-0009 – link to the publication
  4. Tietze Extension Theorem for n-dimensional Spaces

    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (year: 2014, volume: 22(1), pages: 46345), Publisher: University of Białystok
    Status:
    Published
    DOI:
    10.2478/forma-2014-0002 – link to the publication
  5. Improving legibility of natural deduction proofs is not trivial

    Authors:
    K. Pąk
    Academic press:
    Logical Methods in Computer Science (year: 2014, volume: 0,140277777777778, pages: 12055), Publisher: Institute of Theoretical Computer Science of the Technische Universität Braunschweig
    Status:
    Published
    DOI:
    10.2168/LMCS-10(3:23)2014 – link to the publication
  6. Topological Manifolds

    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (year: 2014, volume: 22(2), pages: 179-186), Publisher: University of Białystok
    Status:
    Published
    DOI:
    10.2478/forma-2014-0019 – link to the publication
  7. Improving legibility of formal proofs based on the close reference principle is NP-hard

    Authors:
    K. Pąk
    Academic press:
    Journal of Automated Reasoning (year: 2015, volume: 55, pages: 295-306), Publisher: Springer Science
    Status:
    Published
    DOI:
    10.1007/s10817-015-9337-1 – link to the publication
  8. Bertrand's Ballot Theorem

    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (year: 2014, volume: 22(2), pages: 119-123), Publisher: University of Białystok
    Status:
    Published
    DOI:
    10.2478/forma-2014-0014 – link to the publication

Articles in post-conference publications (6)

  1. Readable Formalization of Euler's Partition Theorem in Mizar

    Authors:
    K. Pąk
    Conference:
    Conferences on Intelligent Computer Mathematics, ścieżka Mathematical Knowledge Management (year: 2015, pages: 211-226), Publisher: Springer
    Date:
    conference 13-17 lipiec
    Status:
    Published
  2. The impact of proof steps sequence on proof readability — experimental setting

    Authors:
    Karol Pąk, Aleksy Schubert
    Conference:
    Conference on Intelligent Computer Mathematics 2016 (year: 2017, pages: 172-186), Publisher: CEUR-WS.org
    Date:
    conference 25-29 lipiec 2016
    Status:
    Published
    DOI:
    link to the publication
  3. Automated Improving of Proof Legibility in the Mizar System

    Authors:
    K. Pąk
    Conference:
    Conferences on Intelligent Computer Mathematics, ścieżka Mathematical Knowledge Management (year: 2014, pages: 373-387), Publisher: Springer
    Date:
    conference 7-11 lipiec 2014
    Status:
    Published
    DOI:
    link to the publication
  4. Lemma Extraction Criteria Based on Properties of Theorem Statements

    Authors:
    Karol Pąk
    Conference:
    Conference on Intelligent Computer Mathematics 2016 (year: 2017, pages: 158-171), Publisher: CEUR-WS.org
    Date:
    conference 25-29 lipiec 2016
    Status:
    Published
    DOI:
    link to the publication
  5. Topological Foundations for a Formal Theory of Manifolds

    Authors:
    Karol Pąk
    Conference:
    Conference on Intelligent Computer Mathematics 2016 (year: 2017, pages: 14-16), Publisher: CEUR-WS.org
    Date:
    conference 25-29 lipiec 2016
    Status:
    Published
    DOI:
    link to the publication
  6. Greedy Algorithms for Finding Maximum Number of Then Step in Reasoning

    Authors:
    Karol Pąk, Aleksy Schubert
    Conference:
    2nd Conference on Artificial Intelligence and Theorem Proving AITP 2017 (year: 2017, pages: 46024), Publisher: Nieznany
    Date:
    conference 26-30 marzec 2017
    Status:
    Published

Book publications / chapters in book publications (1)

  1. Improving Legibility of Proof Scripts Based on Quantity of Introduced Labels

    Authors:
    K. Pąk
    Book:
    Trends in Contemporary Computer Science Podlasie 2014 (year: 2014, volume: -, pages: 71-82), Publisher: Bialystok University of Technology Publishing Office
    Status:
    Published

« New search

Graphic design and implementation: Jakub Piotrowski