4 papers
Stateful Premise Selection by Recurrent Neural Networks
Bartosz Piotrowski, Josef Urban
In this work, we develop a new learning-based method for selecting facts (premises) when proving new goals over large formal libraries. Unlike previous methods that choose sets of…
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Jan Jakubův, Karel Chvalovský, Miroslav Olšák +3
We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems…
Can Neural Networks Learn Symbolic Rewriting?
Bartosz Piotrowski, Josef Urban, Chad E. Brown +1
This work investigates if the current neural architectures are adequate for learning symbolic rewriting. Two kinds of data sets are proposed for this research -- one based on autom…
Guiding Inferences in Connection Tableau by Recurrent Neural Networks
Bartosz Piotrowski, Josef Urban
We present a dataset and experiments on applying recurrent neural networks (RNNs) for guiding clause selection in the connection tableau proof calculus. The RNN encodes a sequence…