Advertisement

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

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

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.

Keywords

Machine learning Theorem proving Kernel methods 
This is a preview of subscription content, log in to check access.

Notes

Acknowledgements

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

References

  1. 1.
    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
  2. 2.
    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/2273702MathSciNetCrossRefGoogle 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), http://arxiv.org/abs/1501.02155
  8. 8.
    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/1e7743302ffe0f0662da24f14c7d5a8fCrossRefGoogle Scholar
  9. 9.
    Paulson, L.C.: Gödel’s incompleteness theorems. Arch. Formal Proofs (2013). http://isa-afp.org/entries/Incompleteness.html, 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). https://doi.org/10.1007/s10817-015-9322-8MathSciNetCrossRefGoogle 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

Cite paper

Buy options