Abstract
We outline a general strategy for the application of edit-distance based kernels to NP Theorem Proving in order to allow for polynomial-time machine learning of proof heuristics without the loss of sequential structural information associated with conventional feature-based machine learning. We provide a general short introduction to logic and proof considering a few important complexity results to set the scene and highlight the relevance of our findings.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Backurs, A., Indyk, P.: Edit distance cannot be computed in strongly subquadratic time (unless SETH is false). CoRR abs/1412.0348 (2014), http://arxiv.org/abs/1412.0348
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979). https://doi.org/10.2307/2273702
Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273–297 (1995)
Das, A.: The Complexity of Propositional Proofs in Deep Inference. Ph.D. thesis, University of Bath Department of Computer Science (2014)
Fischer, A., Uchida, S., Frinken, V., Riesen, K., Bunke, H.: Improving hausdorff edit distance using structural node context. In: International Workshop on Graph-Based Representations in Pattern Recognition, pp. 148–157. Springer, Berlin (2015)
Gonthier, G.: Formal proof—the four color theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008)
Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J.M., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the kepler conjecture. CoRR abs/1501.02155 (2015), http://arxiv.org/abs/1501.02155
Neuhaus, M., Bunke, H.: Edit distance-based kernel functions for structural pattern classification. Pattern Recogn. 39(10), 1852–1863 (2006). http://www.sciencedirect.com/science/article/B6V14-4K48N7S-4/2/1e7743302ffe0f0662da24f14c7d5a8f
Paulson, L.C.: Gödel’s incompleteness theorems. Arch. Formal Proofs (2013). http://isa-afp.org/entries/Incompleteness.html, Formal proof development
Paulson, L.C.: A mechanised proof of gödel’s incompleteness theorems using nominal isabelle. J. Autom. Reasoning 55(1), 1–37 (2015). https://doi.org/10.1007/s10817-015-9322-8
Riesen, K., Fankhauser, S., Bunke, H.: Speeding up graph edit distance computation with a bipartite heuristic
Robinson, J.A.: A machine oriented logic based on the resolution principle. J.ACM 12(1), 23–41 (1965)
Urquhart, A.: The complexity of propositional proofs. Bull. Symbolic Logic 1, 425–467 (1995)
Wallach, H.M.: Topic modeling: beyond bag-of-words. In: Proceedings of the 23rd International Conference on Machine Learning, pp. 977–984. ACM (2006)
Acknowledgements
The first author would like to acknowledge financial support from the Horizon 2020 European Research project DREAMS4CARS (number 731593).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Windridge, D., Kammüller, F. (2020). Edit Distance Kernelization of NP Theorem Proving For Polynomial-Time Machine Learning of Proof Heuristics. In: Arai, K., Bhatia, R. (eds) Advances in Information and Communication. FICC 2019. Lecture Notes in Networks and Systems, vol 70. Springer, Cham. https://doi.org/10.1007/978-3-030-12385-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-12385-7_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-12384-0
Online ISBN: 978-3-030-12385-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)