Skip to main content
SpringerLink
Log in

ULKB Logic: A HOL-Based Framework for Reasoning over Knowledge Graphs

  • Conference paper
  • First Online:
Formal Methods: Foundations and Applications (SBMF 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14414))

Included in the following conference series:

  • 113 Accesses

Abstract

ULKB Logic is an open-source framework written in Python for reasoning over knowledge graphs. It provides an interactive theorem prover-like environment equipped with a higher-order language similar to the one used by HOL Light. The main goal of ULKB Logic is to ease the construction of applications that combine state-of-the-art computational logic tools with the knowledge available in knowledge graphs, such as Wikidata. To this end, the framework provides APIs for fetching statements from SPARQL endpoints and operating over the constructed theories using automated theorem provers and SMT solvers (such as the E prover and Z3). In this paper, we describe the design and implementation of ULKB Logic, its interfaces for querying knowledge graphs and calling external provers, and plans for further development.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/IBM/ULKB.

  2. 2.

    Wikidata is a sister project of Wikipedia and one of the largest publicly available knowledge graphs. WordNet is a comprehensive semantic lexicon for the English language.

  3. 3.

    Type is actually part of ULKB Logic’s standard prelude, which also includes and .

  4. 4.

    The support for type variables distinguishes the variant of simple type theory adopted here from Church’s original formulation [7]. The idea of type variables can be traced back to LCF [10] and provides, within the object language, some of the informal meta-theoretic notations used by Church.

  5. 5.

    The type of is actually

    figure bl

    . ULKB Logic follows the standard practice of assuming “

    figure bm

    ” associates to the right and omits redundant parentheses accordingly. Similarly, application is assumed to associate to the left, i.e.,

    figure bn

    means

    figure bo

    .

  6. 6.

    Predicate is part of the RDF Schema vocabulary (https://www.w3.org/TR/rdf12-schema/); it is used to provide a human-readable name for a resource.

References

  1. Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer, Dordrecht (2002). https://doi.org/10.1007/978-94-015-9934-4

  2. Angles, R., Gutierrez, C.: The expressive power of SPARQL. In: Sheth, A., et al. (eds.) ISWC 2008. LNCS, vol. 5318, pp. 114–129. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88564-1_8

    Chapter  Google Scholar 

  3. Austin, E.C.: HaskHOL: a Haskell hosted domain specific language for higher-order logic theorem proving. Master’s thesis, Electrical Engineering and Computer Science Faculty, University of Kansas (2011)

    Google Scholar 

  4. Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proceedings of 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’08, pp. 3–15. ACM, New York (2008). https://doi.org/10.1145/1328438.1328443

  5. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation and Applications, 2nd edn. Cambridge University Press, Cambridge (2007)

    Google Scholar 

  6. Bansal, K., Loos, S., Rabe, M., Szegedy, C., Wilcox, S.: HOList: an environment for machine learning of higher-order theorem proving. In: Proceedings of 36th International Conference on Machine Learning, Long Beach, California, USA. PMLR (2019)

    Google Scholar 

  7. Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5(2), 56–68 (1940). https://doi.org/10.2307/2266170

    Article  MathSciNet  MATH  Google Scholar 

  8. Dapoigny, R., Barlatier, P.: Modeling ontological structures with type classes in Coq. In: Pfeiffer, H.D., Ignatov, D.I., Poelmans, J., Gadiraju, N. (eds.) ICCS-ConceptStruct 2013. LNCS (LNAI), vol. 7735, pp. 135–152. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35786-2_11

    Chapter  Google Scholar 

  9. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  10. Gordon, M.J.C., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. Springer, Berlin (1979). https://doi.org/10.1007/3-540-09724-4

    Book  MATH  Google Scholar 

  11. Hales, T., et al.: A formal proof of the Kepler conjecture. Forum Math. Pi 5, 1–29 (2017). https://doi.org/10.1017/fmp.2017.1

    Article  MathSciNet  Google Scholar 

  12. Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_4

    Chapter  Google Scholar 

  13. Harrison, J.: HOL Light tutorial (2017). https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf

  14. Horrocks, I., Patel-Schneider, P.F., Boley, H., Tabet, S., Grosof, B., Dean, M.: SWRL: a semantic web rule language combining OWL and RuleML. W3C member submission, W3C, May 2004. https://www.w3.org/Submission/SWRL/

  15. Lai, Z., Ng, A.B., Wong, L.Z., See, S., Lin, S.: Dependently typed knowledge graphs. Technical report. arXiv:2003.03785, arXiv.org (2020)

  16. Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

  17. McBride, C., McKinna, J.: Functional pearl: I am not a number-I am a free variable. In: Proceedings of 2004 ACM SIGPLAN Workshop on Haskell. Haskell ’04, pp. 1–9. ACM, New York (2004). https://doi.org/10.1145/1017472.1017477

  18. Miller, G.A.: WordNet: a lexical database for English. Commun. ACM 38(11), 39–41 (1995). https://doi.org/10.1145/219717.219748

    Article  Google Scholar 

  19. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  20. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  21. Polleres, A., Wallner, J.P.: On the relation between SPARQL 1.1 and answer set programming. J. Appl. Non-Classical Logics 23(1–2), 159–212 (2013). https://doi.org/10.1080/11663081.2013.798992

  22. Pérez, J., Arenas, M., Gutierrez, C.: Semantics and complexity of SPARQL. ACM Trans. Database Syst. 34(3), 16:1–16:45 (2009). https://doi.org/10.1145/1567274.1567278

  23. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2–3), 91–110 (2002)

    MATH  Google Scholar 

  24. Schuler, K.K.: VerbNet: a broad-coverage, comprehensive verb lexicon. Ph.D. thesis, University of Pennsylvania, Philadelphia, PA, USA (2005)

    Google Scholar 

  25. Schulz, S., Cruanes, S., Vukmirović, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495–507. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_29

    Chapter  Google Scholar 

  26. Speer, R., Chin, J., Havasi, C.: ConceptNet 5.5: an open multilingual graph of general knowledge. In: Proceedings of 31st AAAI Conference on Artificial Intelligence (AAAI-17), San Francisco, California, USA, 4–9 February 2017, pp. 4444–4451. AAAI (2017)

    Google Scholar 

  27. Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Automat. Reason. 59(4), 483–502 (2017). https://doi.org/10.1007/s10817-017-9407-7

    Article  MathSciNet  MATH  Google Scholar 

  28. Tang, Y., Sun, J., Dong, J.S., Mahony, B.: Reasoning about semantic web in Isabelle/HOL. In: Proceedings of 11th Asia-Pacific Software Engineering Conference, pp. 46–53 (2004). https://doi.org/10.1109/APSEC.2004.82

  29. The Coq Development Team: The Coq Reference Manual: Release 8.14.0, October 2021

    Google Scholar 

  30. Vrandečić, D., Krötzsch, M.: Wikidata: a free collaborative knowledgebase. Commun. ACM 57(10), 78–85 (2014). https://doi.org/10.1145/2629489

    Article  Google Scholar 

  31. W3C-OWL-WG-2012: OWL 2 web ontology language document overview (second edition). W3C recommendation, W3C, December 2012. http://www.w3.org/TR/2012/REC-owl2-overview-20121211/

  32. W3C SPARQL Working Group: SPARQL 1.1 overview. W3C recommendation, W3C (2013). http://www.w3.org/TR/2013/REC-sparql11-overview-20130321/

  33. Zhan, B.: HolPy: interactive theorem proving in Python. Technical report. arXiv:1905.05970, arXiv.org (2020)

Download references

Author information

Authors and Affiliations

  1. IBM Research Brazil, Rio de Janeiro, Brazil

    Guilherme Lima & Alexandre Rademaker

  2. Getulio Vargas Foundation, School of Applied Mathematics, Rio de Janeiro, Brazil

    Alexandre Rademaker

  3. IBM TJ Watson Research Center, Yorktown Heights, NY, USA

    Rosario Uceda-Sosa

Authors
  1. Guilherme Lima
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexandre Rademaker
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rosario Uceda-Sosa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Guilherme Lima .

Editor information

Editors and Affiliations

  1. Universidade Federal de Minas Gerais, Belo Horizonte, Brazil

    Haniel Barbosa

  2. Bar-Ilan University, Ramat Gan, Israel

    Yoni Zohar

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lima, G., Rademaker, A., Uceda-Sosa, R. (2024). ULKB Logic: A HOL-Based Framework for Reasoning over Knowledge Graphs. In: Barbosa, H., Zohar, Y. (eds) Formal Methods: Foundations and Applications. SBMF 2023. Lecture Notes in Computer Science, vol 14414. Springer, Cham. https://doi.org/10.1007/978-3-031-49342-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-49342-3_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-49341-6

  • Online ISBN: 978-3-031-49342-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation