Theorem Prover for Natural Language

Note: The article is also on author’s other accounts as well.

Hi,

Hope you are doing well.

Here are brief points in summary of the paper “LANGPRO: Natural Language Theorem Prover”, 2017 [1].

This Theorem Prover called LangPro, takes a series of premises that prove the validity of the hypothesis and also presents various relations that exist between them. Here, natural logic, higher-order logic, and a tableau method are used to generate the logic in naturally occurring texts.

— Formal logic, deals with the study of logical truths, propositions, logical inference, and deductive arguments.

— Natural Logic [1] is based on formal logic, higher-order logic where the arguments are mostly linguistic expressions.

— LangPro

It takes as input a set of premises and a hypothesis and processes it with its three major units.

1. CCG Parser
2. LLF Generator, (takes input as trees generated form (1) that is CCG Parser)
3. NLogProver (takes input as LLFs)

— The output generated by LangPro is (1) Entailment, (2) contradictions and (3) neutral to hypothesis.

— Natural Tableau: Here Logic based Analytic Tableau Method is used. This is the tableau method for natural logic. Deductions are drawn, and inference and rules are applied to the logic formulas.

— A tableau rule has an antecedent and has a consequent.

— After each new rule application the new inferred formulas are added in the tableau.

— The tableau rules are often seen as an inverted trees with root as the original formula and it branches out as more rules are applied to the nodes of the tree.

— Closed branches are inconsistent facts.

— Lambda Logical Forms (LLFs) — These are terms of Natural Logic.

— In natural logic, a tableau entry is a tuple of the form (modifier list, an LLF and an argument list, a truth value)

— Natural Tableau searches for counterexamples to prove a statement and either prove it or refute it.

— Generating LLFs, LLFgen— — Natural Tableau would need LLFs as inputs. These LLFs need to be generated form natural text data as input. Also called raw text. LLFgen returns several LLFs.

— Combinatory Categorical Grammar (CCG)– LLFs are produced from this CCG in the following steps. Making CCG terms, unidirectional terms, and creating semantically adequate terms. Type raising of noun phrases is also performed. The authors [1] have written several rules for the above formulations.

— LLFs are obtained from CCGs. Several LLFs are generated from a single CCG tree. This is due to the fact, an np is converted to (vp, s) and there are several quantifiers that are applied while converting a natural text to CCG form.

— LLFgen can be used as an independent module where in FOL and other forms of logics can be applied.

— CCG derivation is predominately done in Prolog. There are ways to get the first LLF only or LLF with certain quantifiers scope.

— NLogPro (The Natural Language Theorem Prover) is an important part of LangPro.

— NLogPro has the following components:

— — Rules (IR), the system has 80 pre-defined rules. Some rules are from logical operations in the form of boolean connectivity, while others are linguistic in nature. Users can define their own rules as well as Prolog rules of form antecedents → consequents form. An example of a user defined rule is:

is_(plant, green)

— — Knowledge Base (KB), this is based out with WordNet 3.0. The WordNet relations in use right now are hypernymy, hyponymy, synonymy, antonymy.

No WSD is performed in this work [1].

— — Proof Engine (PE), here proof trees are built. This involves rules for branching, semantic equivalence, producing and consuming terms. It returns a tree and a list of all its branches.

Finally, LangPro —

It consists of tableau-based theorem prover using CCG parser, LLFgen, and NLogPro. The above modules are applied and results are were produced on textual entailment datasets such as SICK. The use of higher-order logic enhances the working of LangPro and hence the accuracies.

References

[1] Abzianidze, L. (2017). LangPro: Natural language theorem prover. arXiv preprint arXiv:1708.09417.