From Theorem Proving to Cognitive Reasoning

Starting from a depiction of the state of the art in predicate logic theorem proving, we address problems that occur if provers are applied in the wild. In particular, we discuss how automated reasoning systems can be used for natural language question answering. Our approach to tackle common-sense reasoning benchmarks within the Corg project (http://corg.hs-harz.de) is presented, and we demonstrate how word embeddings can help with the problem of axiom selection.