Guiding Inferences in Connection Tableau by Recurrent Neural Networks

Gauthier, T.: Deep reinforcement learning for synthesizing functions in higher-order logic. CoRR (2019), http://arxiv.org/abs/1910.11797

Original

1910

Earlier work this paper cites.

Piotrowski, B., Urban, J., Brown, C.E., Kaliszyk, C.: Can neural networks learn symbolic rewriting? CoRR (2019), https://arxiv.org/pdf/1911.04873.pdf

Original

1911

Earlier work this paper cites.

Lample, G., Charton, F.: Deep learning for symbolic mathematics. CoRR (2019), http://arxiv.org/abs/1912.01412

Original

1912

Earlier work this paper cites.

Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection tableau calculi. J. Autom. Reasoning 13

1994

Earlier work this paper cites.

Otten, J., Bibel, W.: leanCoP: Lean connection-based theorem proving. J. Symbolic Computation 36

2003

Earlier work this paper cites.

Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Automated Reasoning 37

2006

Earlier work this paper cites.

Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3

2010

Cited alongside, same era.

Cho, K., van Merrienboer, B., Gülçehre, Ç., Bahdanau, D., Bougares, F., Schwenk, H., Bengio, Y.: Learning phrase representations using RNN encoder-decoder for statistical machine translation. In: EMNLP 2014, pp. 1724–1734 (2014)

2014

Cited alongside, same era.

Chen, T., Guestrin, C.: XGBoost: A scalable tree boosting system. In: ACM SIGKDD 2016, pp. 785–794 (2016)

2016

Cited alongside, same era.

Freitag, M., Al-Onaizan, Y.: Beam search strategies for neural machine translation. In: NMT@ACL 2017, pp. 56–60 (2017)

2017

Cited alongside, same era.

Kaliszyk, C., Chollet, F., Szegedy, C.: Holstep: A machine learning dataset for higher-order logic theorem proving. In: ICLR 2017 (2017)

2017

Cited alongside, same era.

Luong, M., Brevdo, E., Zhao, R.: Neural machine translation (seq2seq) tutorial (2017), https://github.com/tensorflow/nmt

2017

Later among the works it cites.

Evans, R., Saxton, D., Amos, D., Kohli, P., Grefenstette, E.: Can neural networks understand logical entailment? In: ICLR 2018 (2018)

2018

Later among the works it cites.

Kaliszyk, C., Urban, J., Michalewski, H., Olsák, M.: Reinforcement learning of theorem proving. In: NeurIPS 2018, pp. 8836–8847 (2018)

2018

Later among the works it cites.

Wang, Q., Kaliszyk, C., Urban, J.: First experiments with neural translation of informal to formal mathematics. In: CICM 2018, pp. 255–270 (2018)

Original

2018

Later among the works it cites.

Chvalovský, K., Jakubuv, J., Suda, M., Urban, J.: ENIGMA-NG: Efficient neural and gradient-boosted inference guidance for E. In: CADE 27, pp. 197–215 (2019)