A Pure Logic-Based Approach to Natural Reasoning

Abstract

The paper presents a model for natural reasoning that combines theorem proving techniques with natural logic. The model is a tableau system for a higher-order logic the formulas of which resemble linguistic expressions. A textual entailment system LangPro, an implementation of the model, represents a tableau-based prover that directly operates on linguistic expressions. After training and evaluating on a textual entailment dataset, the prover shows accuracy comparable to the state-of-the-art results with almost perfect precision. Due to its reliable judgements, the system is also able to detect dubious problems in the dataset.