LangPro: Natural Language Theorem Prover
This addresses the problem of semantic reasoning in natural language processing for researchers and practitioners, though it appears incremental as it builds on existing methods for natural logic.
The authors tackled the problem of automated theorem proving for natural language by developing LangPro, a prover based on an analytic tableau method for natural logic, which achieved high results comparable to state-of-the-art on the FraCaS and SICK textual entailment datasets.
LangPro is an automated theorem prover for natural language (https://github.com/kovvalsky/LangPro). Given a set of premises and a hypothesis, it is able to prove semantic relations between them. The prover is based on a version of analytic tableau method specially designed for natural logic. The proof procedure operates on logical forms that preserve linguistic expressions to a large extent. %This property makes the logical forms easily obtainable from syntactic trees. %, in particular, Combinatory Categorial Grammar derivation trees. The nature of proofs is deductive and transparent. On the FraCaS and SICK textual entailment datasets, the prover achieves high results comparable to state-of-the-art.