Combining Theorem Proving with Natural Language Processing

Abstract. The LogAnswer system is an application of automated reasoning to the field of open domain question-answering, the retrieval of answers to natural language questions regarding arbitrary topics. In our system we have integrated an automated theorem prover in a framework of natural language processing tools to allow for deductive reasoning over an extensive knowledge base derived from textual sources. For this purpose we had to intertwine two opposing approaches: on the one hand formal logic with its brittle precision, and on the other hand, machine learning applied to shallow linguistic features, which is robust but less precise. In the paper we will present implementation details as well as obstacles and their solutions.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Björn Pelzer, Ingo Glöckner
• Keywords: Automated Reasoning, CADE 2008, Extensive Knowledge Base, Hand Formal Logic, Language Processing Tools