LangPro: Natural Language Theorem Prover

TL;DR

LangPro is an automated theorem prover for natural language that uses a specialized analytic tableau method on logical forms derived from syntactic trees, achieving high accuracy on textual entailment datasets.

Contribution

It introduces a novel natural logic-based tableau prover that operates on linguistic-preserving logical forms, enabling transparent and effective semantic reasoning.

Findings

Achieves high accuracy on FraCaS and SICK datasets

Operates on logical forms closely aligned with linguistic expressions

Provides transparent, deductive proofs

Abstract

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.