Lasha Abzianidze: A Natural Language Theorem Prover
The paper presents an automated theorem prover that is able to check natural language arguments for (in)validity and a~set~of sentences for (in)consistency.
The actual proof procedure acts on
formulas that are simply-typed lambda-terms with lexical constants that resemble English phrases;
the terms are obtained from the parse trees generated by the C&C tools.
The nature of proofs are deductive and, at the same time, transparent.
The prover obtains comparable accuracy on the SICK and FraCaS textual entailment data sets while showing almost perfect precision.