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
Principal investigator (from the host institution)
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]
- Laptop min. czterordzeniowy, dodatkowy monitor.. Cost: 5 000 PLN
Information in the final report
Publication in academic press/journals (8)
-
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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)
-
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
-
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
-
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
-
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
-
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
-
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)
-
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