Projects funded by the NCN


Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Algorithms concerning the legibility of natural deduction proofs

2012/07/N/ST6/02147

Keywords:

Operations on languages Legibility of proofs Acyclic partition digraph Linear arrangement NP-complete probleb

Descriptors:

  • ST6_4: Formal methods, foundations of computer science, including theoretical computer science, quantum algorithms
  • ST6_6: Algorithms, parallel, distributed and network algorithms, algorithmic game theory

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

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

Call: PRELUDIUM 4 - announced on 2012-09-15

Amount awarded: 98 340 PLN

Project start date (Y-m-d): 2013-07-08

Project end date (Y-m-d): 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. (5 000 PLN)

Information in the final report

  • Publication in academic press/journals (8)
  • Articles in post-conference publications (6)
  • Book publications / chapters in book publications (1)
  1. Tietze Extension Theorem for n-dimensional Spaces
    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (rok: 2014, tom: 22(1), strony: 45615), Wydawca: University of Białystok
    Status:
    Published
    DOI:
    10.2478/forma-2014-0002 - link to the publication
  2. Topological Manifolds
    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (rok: 2014, tom: 22(2), strony: 179-186), Wydawca: University of Białystok
    Status:
    Published
    DOI:
    10.2478/forma-2014-0019 - link to the publication
  3. Flexary Operations
    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (rok: 2015, tom: 32(2), strony: 81-92), Wydawca: University of Białystok
    Status:
    Published
    DOI:
    10.1515/forma-2015-0008 - link to the publication
  4. Improving legibility of formal proofs based on the close reference principle is NP-hard
    Authors:
    K. Pąk
    Academic press:
    Journal of Automated Reasoning (rok: 2015, tom: 55, strony: 295-306), Wydawca: Springer Science
    Status:
    Published
    DOI:
    10.1007/s10817-015-9337-1 - link to the publication
  5. Bertrand's Ballot Theorem
    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (rok: 2014, tom: 22(2), strony: 119-123), Wydawca: University of Białystok
    Status:
    Published
    DOI:
    10.2478/forma-2014-0014 - link to the publication
  6. Euler's Partition Theorem
    Authors:
    K. Pąk
    Academic press:
    Formalized Mathematics (rok: 2015, tom: 23(2), strony: 93-99), Wydawca: University of Białystok
    Status:
    Published
    DOI:
    10.1515/forma-2015-0009 - link to the publication
  7. Improving legibility of natural deduction proofs is not trivial
    Authors:
    K. Pąk
    Academic press:
    Logical Methods in Computer Science (rok: 2014, tom: 0,140277777777778, strony: 12055), Wydawca: 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
  8. Leibniz Series for PI
    Authors:
    Karol Pąk
    Academic press:
    Formalized Mathematics (rok: 2016, tom: 24, strony: 275–280), Wydawca: Uniwersytet w Białymstoku
    Status:
    Published
    DOI:
    10.1515/forma-2016-0023 - link to the publication
  1. Automated Improving of Proof Legibility in the Mizar System
    Authors:
    K. Pąk
    Conference:
    Conferences on Intelligent Computer Mathematics, ścieżka Mathematical Knowledge Management (rok: 2014, ), Wydawca: Springer
    Data:
    konferencja 7-11 lipiec 2014
    Status:
    Published
  2. Topological Foundations for a Formal Theory of Manifolds
    Authors:
    Karol Pąk
    Conference:
    Conference on Intelligent Computer Mathematics 2016 (rok: 2017, ), Wydawca: CEUR-WS.org
    Data:
    konferencja 25-29 lipiec 2016
    Status:
    Published
  3. Lemma Extraction Criteria Based on Properties of Theorem Statements
    Authors:
    Karol Pąk
    Conference:
    Conference on Intelligent Computer Mathematics 2016 (rok: 2017, ), Wydawca: CEUR-WS.org
    Data:
    konferencja 25-29 lipiec 2016
    Status:
    Published
  4. Readable Formalization of Euler's Partition Theorem in Mizar
    Authors:
    K. Pąk
    Conference:
    Conferences on Intelligent Computer Mathematics, ścieżka Mathematical Knowledge Management (rok: 2015, ), Wydawca: Springer
    Data:
    konferencja 13-17 lipiec
    Status:
    Published
  5. 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 (rok: 2017, ), Wydawca: Nieznany
    Data:
    konferencja 26-30 marzec 2017
    Status:
    Published
  6. The impact of proof steps sequence on proof readability — experimental setting
    Authors:
    Karol Pąk, Aleksy Schubert
    Conference:
    Conference on Intelligent Computer Mathematics 2016 (rok: 2017, ), Wydawca: CEUR-WS.org
    Data:
    konferencja 25-29 lipiec 2016
    Status:
    Published
  1. Improving Legibility of Proof Scripts Based on Quantity of Introduced Labels
    Authors:
    K. Pąk
    Book:
    Trends in Contemporary Computer Science Podlasie 2014 (rok: 2014, tom: -, strony: 71-82), Wydawca: Bialystok University of Technology Publishing Office
    Status:
    Published