{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T22:18:55Z","timestamp":1775254735485,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030027674","type":"print"},{"value":"9783030027681","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02768-1_17","type":"book-chapter","created":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:42:27Z","timestamp":1540107747000},"page":"309-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks"],"prefix":"10.1007","author":[{"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7466-8789","authenticated-orcid":false,"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"17_CR1","unstructured":"Avellone, A., Fiorino, G., Moscato, U.: A new $$O(n \\log {n})$$-space decision procedure for propositional intuitionistic logic. Kurt G\u00f6del Society Collegium Logicum VIII, 17\u201333 (2004)"},{"key":"17_CR2","unstructured":"Bahdanau, D., Cho, K., Bengio, Y.: Neural machine translation by jointly learning to align and translate. CoRR abs\/1409.0473 (2014)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M Barnett","year":"2008","unstructured":"Barnett, M., et al.: The Spec# programming system: challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144\u2013152. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69149-5_16"},{"key":"17_CR4","unstructured":"Ben-Yelles, C.: Type assignment in the lambda-calculus: syntax and semantics. Ph.D. thesis, University College of Swansea, September 1979"},{"key":"17_CR5","unstructured":"Bibel, W.: Automated Theorem Proving. Springer, Heidelberg (2013)"},{"key":"17_CR6","unstructured":"B\u00fcnz, B., Lamm, M.: Graph neural networks and boolean satisfiability. CoRR abs\/1702.03592 (2017)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Chalin, P., James, P.R., Karabotsos, G.: An integrated verification environment for JML: architecture and early results. In: Proceedings of SAVCBS, pp. 47\u201353. ACM, New York (2007)","DOI":"10.1145\/1292316.1292322"},{"key":"17_CR8","unstructured":"Evans, R., Saxton, D., Amos, D., Kohli, P., Grefenstette, E.: Can neural networks understand logical entailment? CoRR abs\/1802.08535 (2018)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF00344251","volume":"36","author":"K Fukushima","year":"1980","unstructured":"Fukushima, K.: Neocognitron: a self-organizing neural network for a mechanism of pattern recognition unaffected by shift in position. Biol. Cybern. 36, 193\u2013202 (1980)","journal-title":"Biol. Cybern."},{"key":"17_CR11","unstructured":"Glorot, X., Bordes, A., Bengio, Y.: Deep sparse rectifier neural networks. In: Proceedings of AISTATS, pp. 315\u2013323 (2011)"},{"key":"17_CR12","volume-title":"Deep Learning","author":"I Goodfellow","year":"2016","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: Proceedings of CVPR, pp. 770\u2013778 (2016)","DOI":"10.1109\/CVPR.2016.90"},{"issue":"6","key":"17_CR15","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/MSP.2012.2205597","volume":"29","author":"G Hinton","year":"2012","unstructured":"Hinton, G., et al.: Deep neural networks for acoustic modeling in speech recognition: the shared views of four research groups. IEEE Sig. Process. Mag. 29(6), 82\u201397 (2012)","journal-title":"IEEE Sig. Process. Mag."},{"key":"17_CR16","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., E\u00e9n, N., Chollet, F., Urban, J.: DeepMath - deep sequence models for premise selection. In: Proceedings of NIPS, pp. 2235\u20132243 (2016)"},{"issue":"2","key":"17_CR17","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1016\/0743-7315(89)90068-3","volume":"6","author":"JL Johnson","year":"1989","unstructured":"Johnson, J.L.: A neural network approach to the 3-satisfiability problem. J. Parallel Distrib. Comput. 6(2), 435\u2013449 (1989)","journal-title":"J. Parallel Distrib. Comput."},{"key":"17_CR18","unstructured":"Kaliszyk, C., Chollet, F., Szegedy, C.: HolStep: a machine learning dataset for higher-order logic theorem proving. CoRR abs\/1703.00426 (2017)"},{"key":"17_CR19","unstructured":"Kingma, D.P., Ba, J.: Adam: a method for stochastic optimization. CoRR abs\/1412.6980 (2014)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of SOSP, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"17_CR21","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Proceedings of NIPS, pp. 1106\u20131114 (2012)"},{"issue":"7","key":"17_CR22","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Proceedings of LPAR, pp. 85\u2013105 (2017)","DOI":"10.29007\/8mwc"},{"issue":"3","key":"17_CR24","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Mou, L., Li, G., Zhang, L., Wang, T., Jin, Z.: Convolutional neural networks over tree structures for programming language processing. In: Proceedings of AAAI, pp. 1287\u20131293 (2016)","DOI":"10.1609\/aaai.v30i1.10139"},{"issue":"1\u20133","key":"17_CR26","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. J. Autom. Reason. 38(1\u20133), 261\u2013271 (2007)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"17_CR27","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/TNN.2008.2005605","volume":"20","author":"F Scarselli","year":"2009","unstructured":"Scarselli, F., Gori, M., Tsoi, A.C., Hagenbuchner, M., Monfardini, G.: The graph neural network model. IEEE Trans. Neural Netw. 20(1), 61\u201380 (2009)","journal-title":"IEEE Trans. Neural Netw."},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"key":"17_CR29","unstructured":"Sekiyama, T., Imanishi, A., Suenaga, K.: Towards proof synthesis guided by neural machine translation for intuitionistic propositional logic. CoRR abs\/1706.06462 (2017)"},{"key":"17_CR30","unstructured":"Sekiyama, T., Suenaga, K.: Automated proof synthesis for propositional logic with deep neural networks. CoRR abs\/1805.11799 (2018). http:\/\/arxiv.org\/abs\/1805.11799"},{"key":"17_CR31","unstructured":"Selsam, D., Lamm, M., B\u00fcnz, B., Liang, P., de Moura, L., Dill, D.L.: Learning a SAT solver from single-bit supervision. CoRR abs\/1802.03685 (2018)"},{"key":"17_CR32","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/S0049-237X(06)80018-2","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"M.H. S\u00f8rensen","year":"2006","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol. 149. Elsevier Science Inc., Amsterdam (2006)"},{"key":"17_CR33","unstructured":"Sutskever, I., Vinyals, O., Le, Q.V.: Sequence to sequence learning with neural networks. In: Proceedings of NIPS, pp. 3104\u20133112 (2014)"},{"key":"17_CR34","unstructured":"Tokui, S., Oono, K., Hido, S., Clayton, J.: Chainer: a next-generation open source framework for deep learning. In: Proceedings of workshop on LearningSys (2015)"},{"key":"17_CR35","unstructured":"Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Proceedings of NIPS, pp. 2783\u20132793 (2017)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02768-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T20:57:25Z","timestamp":1775249845000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02768-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030027674","9783030027681"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02768-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wellington","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/aplas2018.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}