Skip to main content

Automated Reasoning in the Wild

  • Conference paper
  • First Online:
Automated Deduction - CADE-25 (CADE 2015)

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

Included in the following conference series:

Abstract

This paper discusses the use of first order automated reasoning in question answering and cognitive computing. For this the natural language question answering project LogAnswer is briefly depicted and the challenges faced therein are addressed. This includes a treatment of query relaxation, web-services, large knowledge bases and co-operative answering. In a second part a bridge to human reasoning as it is investigated in cognitive psychology is constructed by using standard deontic logic.

Work supported by DFG FU 263/15-1 ‘Ratiolog’.

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

Access this chapter

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.

    Rudy Giuliani was the mayor of which city in the USA?

  2. 2.

    Responsible for the charges was the future mayor of New York, Rudolph Giuliani.

  3. 3.

    http://dbpedia.org/.

  4. 4.

    Screenshot available at: http://orphanfilmsymposium.blogspot.com/2008/05/national-science-foundation-grants.html (retrieved: 21st of april 2015).

  5. 5.

    We are aware that this formalization is too strong since it causes someone only to be disappointed if he is never defended in the future. However, in the Triangle-COPA, the future only consists of a very small number of events and therefore this formalization is sufficient for our purposes.

References

  1. Baumgartner, P., Furbach, U., Groß-Hardt, M., Sinner, A.: Living book - deduction, slicing, and interaction. J. Autom. Reasoning 32(3), 259–286 (2004)

    Article  Google Scholar 

  2. Baumgartner, P., Furbach, U., Pelzer, B.: Hyper tableaux with equality. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 492–507. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Beckert, B., Hähnle, R.: Reasoning and verification: state of the art and current trends. IEEE Intell. Syst. 29(1), 20–29 (2014)

    Article  Google Scholar 

  4. Byrne, R.M.J.: Suppressing valid inferences with conditionals. Cognition 31(1), 61–83 (1989)

    Article  MathSciNet  Google Scholar 

  5. Ferrucci, D., Levas, A., Bagchi, S., Gondek, D., Mueller, E.T.: Watson: beyond jeopardy!. Artif. Intell. 199–200, 93–105 (2013)

    Article  Google Scholar 

  6. Furbach, U., Glöckner, I., Pelzer, B.: An application of automated reasoning in natural language question answering. AI Commun. 23(2–3), 241–265 (2010)

    MathSciNet  MATH  Google Scholar 

  7. Furbach, U., Schon, C.: Deontic logic for human reasoning. In: Eiter, T., Strass, H., Truszczyński, M., Woltran, S. (eds.) Advances in Knowledge Representation. LNCS, vol. 9060, pp. 63–80. Springer, Heidelberg (2015)

    Google Scholar 

  8. Furbach, U., Schon, C., Stolzenburg, F., Weis, K.-H., Wirth, C.-P.: The RatioLog Project - Rational Extensions of Logical Reasoning. ArXiv e-prints, March 2015

    Google Scholar 

  9. Gabbay, D., Horty, J., Parent, X., van der Meyden, R., van der Torre, L. (eds.): Handbook of Deontic Logic and Normative Systems. College Publications, London (2013)

    MATH  Google Scholar 

  10. Heider, F., Simmel, M.: An experimental study of apparent behavior. Am. J. Psychol. 57(2), 243–259 (1944)

    Article  Google Scholar 

  11. Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299–314. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  12. Hölldobler, S., Philipp, T., Wernhard, C.: An abductive model for human reasoning. In: AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning (2011)

    Google Scholar 

  13. Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning 53(2), 173–213 (2014)

    Article  MathSciNet  Google Scholar 

  14. Kowalski, R.: Computational Logic and Human Thinking: How to be Artificially Intelligent. Cambridge University Press, Cambridge (2011)

    Book  Google Scholar 

  15. Levesque, H.J.: The winograd schema challenge. In: LogicalFormalizations of Commonsense Reasoning, Papers from the 2011 AAAI Spring Symposium, Technical Report SS-11-06, Stanford, California, USA, 21–23 March 2011. AAAI (2011)

    Google Scholar 

  16. Maslan, N., Roemmele, M., Gordon, A.S.: One hundred challenge problems for logical formalizations of commonsense psychology. In: Twelfth International Symposium on Logical Formalizations of Commonsense Reasoning, Stanford, CA (2015)

    Google Scholar 

  17. McCune, W.: OTTER 3.3 Reference Manual. Argonne National Laboratory, Argonne, Illinois (2003)

    Google Scholar 

  18. Pelzer, B.: Automated Reasoning Embedded in Question Answering. Ph.D. thesis, University of Koblenz (2013)

    Google Scholar 

  19. Pelzer, B.: Automated theorem proving with web services. In: Timm, I.J., Thimm, M. (eds.) KI 2013. LNCS, vol. 8077, pp. 152–163. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  20. Roemmele, M., Bejan, C.A., Gordon, A.S.: Choice of plausible alternatives: an evaluation of commonsense causal reasoning. In: Logical Formalizations of Commonsense Reasoning,Papers from the 2011 AAAI Spring Symposium, Technical Report SS-11-06, Stanford, California, USA, 21–23 March 2011. AAAI (2011)

    Google Scholar 

  21. Shankar, N.: Automated reasoning, fast and slow. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 145–161. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  22. Stenning, K., Van Lambalgen, M.: Human Reasoning and Cognitive Science. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  23. Suda, M., Sutcliffe, G., Wischnewski, P., Lamotte-Schubert, M., de Melo, G.: External sources of axioms in automated theorem proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS, vol. 5803, pp. 281–288. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009)

    Article  MATH  Google Scholar 

  25. Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: Malarea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  26. von Kutschera, F.: Einführung in die Logik der Normen. Werte und Entscheidungen, Alber (1973)

    Google Scholar 

  27. Wason, P.C.: Reasoning about a rule. Q. J. Exp. Psychol. 20(3), 273–281 (1968)

    Article  Google Scholar 

  28. Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System sescription: spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 514–520. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  29. Wos, L., Overbeek, R., Lusk, E., Boyle, J.: Automated Reasoning: Introduction and Applications. Prentice-Hall, Englewood Cliffs (1984)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Ulrich Furbach .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Furbach, U., Pelzer, B., Schon, C. (2015). Automated Reasoning in the Wild. In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-21401-6_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-21400-9

  • Online ISBN: 978-3-319-21401-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics