Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2019: Automated Deduction – CADE 27 pp 538–549Cite as

GKC: A Reasoning System for Large Knowledge Bases

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11716))

Abstract

This paper introduces GKC, a resolution prover optimized for search in large knowledge bases. The system is built upon a shared memory graph database Whitedb, enabling it to solve multiple different queries without a need to repeatedly parse or load the large parsed knowledge base from the disk. Due to the relatively shallow and simple structure of most of the literals in the knowledge base, the indexing methods used are mostly hash-based. While GKC performs well on large problems from the TPTP set, the system is built for use as a core system for developing a toolset of commonsense reasoning functionalities.

This is a preview of subscription content, 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   69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   89.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

Learn about institutional subscriptions

References

  1. TPTP homepage. http://tptp.cs.miami.edu/~tptp/

  2. Tammet, T.: Gandalf. J. Autom. Reason. 18(2), 199–204 (1997)

    Article  Google Scholar 

  3. Tammet, T.: Towards efficient subsumption. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 427–441. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054276

    Chapter  Google Scholar 

  4. Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, vol. 257, pp. 61–70. CEUR Workshop Proceedings (2007)

    Google Scholar 

  5. Reagan, S.P., Sutcliffe, G., Goolsbey, K., Kahlert, R.C.: The Cyc TPTP Challenge Problem Set. Unpublished manuscript. http://www.opencyc.org/doc/tptp_challenge_problem_set

  6. Suchanek, F., Kasneci, G.m Weikum, G.: YAGO: a core of semantic knowledge. In: Proceedings of the 16th International World Wide Web Conference, Banff, Canada, pp. 697–706

    Google Scholar 

  7. Sutcliffe, G.: The TPTP world – infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 1–12. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_1

    Chapter  Google Scholar 

  8. Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 441–456. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_38

    Chapter  Google Scholar 

  9. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, pp. 19–99. Elsevier (2001)

    Google Scholar 

  10. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  11. Schulz, S., Möhrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 330–345. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_23

    Chapter  Google Scholar 

  12. Sekar, R., Ramakrishnan, I., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning, vol. II, chap. 26, pp. 1853–1964. Elsevier Science (2001)

    Google Scholar 

  13. Schulz, S.: Simple and efficient clause subsumption with feature vector indexing. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 45–67. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36675-8_3

    Chapter  Google Scholar 

  14. Tammet, T., Järv, P.: WhiteDB homepage. https://whitedb.org

  15. Furbach, U., Schon, C.: Commonsense reasoning meets theorem proving. In: Proceedings of the Workshop on Bridging the Gap between Human and Automated Reasoning co-located with 25th International Joint Conference on Artificial Intelligence IJCAI 2016, pp. 74–85. CEUR (2016)

    Google Scholar 

  16. Sutcliffe, G.: The 9th IJCAR automated theorem proving system competition - CASC-J9. AI Commun. 31(1), 1–13 (2018)

    Article  MathSciNet  Google Scholar 

  17. Lopez Hernandez, J.C., Korovin, K.: An abstraction-refinement framework for reasoning with large theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 663–679. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_43

    Chapter  MATH  Google Scholar 

  18. Tammet, T.: Repository of the GKC system and experiment logs (2019). https://github.com/tammet/gkc

Download references

Author information

Authors and Affiliations

  1. Tallinn University of Technology, Tallinn, Estonia

    Tanel Tammet

Authors
  1. Tanel Tammet
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tanel Tammet .

Editor information

Editors and Affiliations

  1. University of Lorraine, Villers-lès-Nancy, France

    Pascal Fontaine

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Tammet, T. (2019). GKC: A Reasoning System for Large Knowledge Bases. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29436-6_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29435-9

  • Online ISBN: 978-3-030-29436-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation