Edit Distance Kernelization of NP Theorem Proving For Polynomial-Time Machine Learning of Proof Heuristics

  • David WindridgeEmail author
  • Florian Kammüller
Conference paper
Part of the Lecture Notes in Networks and Systems book series (LNNS, volume 70)


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.


Machine learning Theorem proving Kernel methods 



The first author would like to acknowledge financial support from the Horizon 2020 European Research project DREAMS4CARS (number 731593).


  1. 1.
    Backurs, A., Indyk, P.: Edit distance cannot be computed in strongly subquadratic time (unless SETH is false). CoRR abs/1412.0348 (2014),
  2. 2.
    Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979). Scholar
  3. 3.
    Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273–297 (1995)zbMATHGoogle Scholar
  4. 4.
    Das, A.: The Complexity of Propositional Proofs in Deep Inference. Ph.D. thesis, University of Bath Department of Computer Science (2014)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Gonthier, G.: Formal proof—the four color theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008)MathSciNetzbMATHGoogle Scholar
  7. 7.
    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),
  8. 8.
    Neuhaus, M., Bunke, H.: Edit distance-based kernel functions for structural pattern classification. Pattern Recogn. 39(10), 1852–1863 (2006). Scholar
  9. 9.
    Paulson, L.C.: Gödel’s incompleteness theorems. Arch. Formal Proofs (2013)., Formal proof development
  10. 10.
    Paulson, L.C.: A mechanised proof of gödel’s incompleteness theorems using nominal isabelle. J. Autom. Reasoning 55(1), 1–37 (2015). Scholar
  11. 11.
    Riesen, K., Fankhauser, S., Bunke, H.: Speeding up graph edit distance computation with a bipartite heuristicGoogle Scholar
  12. 12.
    Robinson, J.A.: A machine oriented logic based on the resolution principle. J.ACM 12(1), 23–41 (1965)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Urquhart, A.: The complexity of propositional proofs. Bull. Symbolic Logic 1, 425–467 (1995)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Wallach, H.M.: Topic modeling: beyond bag-of-words. In: Proceedings of the 23rd International Conference on Machine Learning, pp. 977–984. ACM (2006)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Middlesex University LondonLondonUK

Personalised recommendations