Deep Neural Architectures for Automated Theorem Proving
2018/29/N/ST6/02903
Keywords
Descriptors
- ST6_7: Sztuczna inteligencja, systemy inteligentne i wieloagentowe
- ST6_11: Uczenie maszynowe, statystyczne przetwarzanie danych i zastosowanie w przetwarzaniu sygnałów
- ST6_4: Metody formalne, teoretyczne podstawy informatyki w tym informatyka teoretyczna
Panel
ST6 – Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems
Host institution
Uniwersytet Warszawski, Wydział Matematyki, Informatyki i Mechaniki
Voivodeship: mazowieckie
Principal investigator (from the host institution)
Number of co-investigators in the project: 2
Call
PRELUDIUM 15 – announced on 2018-03-15
- Amount awarded
- 119 100 PLN
- Project start date
- 2019-01-24
- Project end date
- 2023-01-23
- Project duration
- 48 months (the same as in the proposal)
- Project status
- Project settled
Project description
Download the project description in a pdf file
Note — project descriptions were prepared by the authors of the applications themselves and placed in the system in an unchanged form.
Equipment purchased [PL]
- Karta graficzna NVIDIA GeForce GTX 1080 Ti (lub podobna). Cost: 4 000 PLN
- Stacja robocza. Cost: 8 000 PLN
Information in the final report
Articles in post-conference publications (4)
-
Stateful Premise Selection by Recurrent Neural Networks
- Authors:
- Bartosz Piotrowski, Josef Urban
- Conference:
- 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (year: 2020, pages: 409-422), Publisher: EPiC Series in Computing
- Date:
- conference 43973
- Status:
- Published
-
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine
- Authors:
- Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
- Conference:
- Automated Reasoning - 10th International Joint Conference (year: 2020, pages: 448-463), Publisher: Springer
- Date:
- conference 44013
- Status:
- Published
-
Guiding Inferences in Connection Tableau by Recurrent Neural Networks
- Authors:
- Bartosz Piotrowski, Josef Urban
- Conference:
- 13th Conference on Intelligent Computer Mathematics (year: 2020, pages: 309-314), Publisher: Springer LNCS
- Date:
- conference 44038
- Status:
- Published
-
MizAR 60 for Mizar 50
- Authors:
- Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
- Conference:
- Fourteenth Conference on Interactive Theorem Proving (year: 2023), Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- Status:
- Accepted for publication