# LangPro: Natural Language Theorem Prover

arXiv: https://arxiv.org/abs/1708.09417 · HTML: https://mlsanity.com/paper/1708.09417/

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Aug 2017.

## Built on by (most cited first, 15 of 15)

- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [ProoFVer: Natural Logic Theorem Proving for Fact Verification](https://mlsanity.com/paper/2108.11357/) (2021)
- [NeuralLog: Natural Language Inference with Joint Neural and Logical Reasoning](https://mlsanity.com/paper/2105.14167/) (2021)
- [Logical Reasoning with Span-Level Predictions for Interpretable and Robust NLI Models](https://mlsanity.com/paper/2205.11432/) (2022)
- [RECKONING: Reasoning through Dynamic Knowledge Encoding](https://mlsanity.com/paper/2305.06349/) (2023)
- [NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models](https://mlsanity.com/paper/2602.13237/) (2026)
- [Decomposing Natural Logic Inferences in Neural NLI](https://mlsanity.com/paper/2112.08289/) (2021)
- [Monotonicity Marking from Universal Dependency Trees](https://mlsanity.com/paper/2104.08659/) (2021)
- [forallutoexistsval: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks](https://mlsanity.com/paper/2403.18327/) (2024)
- [Logic Agent: Enhancing Validity with Logic Rule Invocation](https://mlsanity.com/paper/2404.18130/) (2024)
- [SPINDLE: Spinning Raw Text into Lambda Terms with Graph Attention](https://mlsanity.com/paper/2302.12050/) (2023)
- [Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference](https://mlsanity.com/paper/2311.08637/) (2023)
- [A Logic-Based Framework for Natural Language Inference in Dutch](https://mlsanity.com/paper/2110.03323/) (2021)
- [Linguistic Features for Interpretable Textual Entailment](https://mlsanity.com/paper/2609.24932/) (2026)
- [Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs](https://mlsanity.com/paper/2609.32491/) (2026)

## Abstract (arXiv)

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.