Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference

In this position paper, we propose a reasoning framework that can model the reasoning process underlying natural language inferences. The framework is based on the semantic tableau method, a well-studied proof system in formal logic. Like the semantic tableau, the framework is driven by refutation -- something is proved if and only if its counterexample was not refuted. Despite being rooted in formal logic, the framework shares similarities with the mental models, a theory on the psychology of reasoning. We will show how the reasoning framework can facilitate the collection of comprehensive and structured explanations for existing naturalistic inference problems. To make the suggestion more concrete, we propose a method of semi-automatically obtaining structured explanations from the formal proofs of a reliable and high-performing logic-based inference system. Taking advantage of the in-depth information available in the generated formal proofs, we show how it can be used to define natural language reasoning tasks with structured explanations. The proposed tasks can be ordered according to difficulty defined in terms of the granularity of explanations. We argue that the tasks that contain a natural sketch of the proofs will suffer from substantially fewer shortcomings than the existing explainable reasoning tasks (or datasets).