LangPro
: Natural Language Theorem Prover
LangPro tries to find out a semantic relation between
a set of premises and a hypothesis.
The semantic relation can be:
entailment/yes,
contradiction/no,
neutral/unknown.
LangPro obtains competetive results on the SICK and FraCaS RTE (i.e. recognizing textual entailment) datasets.
The version used for the demo is outdated. Consult the GitHub repo for the recent version of LangPro.
The inputs to the prover are recorded
LangPro obtains competetive results on the SICK and FraCaS RTE (i.e. recognizing textual entailment) datasets.
The version used for the demo is outdated. Consult the GitHub repo for the recent version of LangPro.
The inputs to the prover are recorded
LangPro produces Lambda Logical Forms (LLFs) from CCG derivations.
The CCG derivations are produced by the C&C and EasyCCG parsers.
You can choose both parsers and LangPro will consider LLFs based on the derivations from each parser.
Do not forget to choose at least one parser.
For each argument, LangPro automatically generates a knowledge base from WordNet.
The tab for the SICK problems loads slowly as it contains 4.5K problems.
Processing a user input takes more time as parsers are loaded to parse the input.
There are two types of open tableaux.
If no rule application can be carried out on its open branches, an open tableau is terminated,
otherwise it is limited, i.e. the rule application limit is reached and it forbids further rule applications.
The intuition behind tableau nodes:
node id
list of modifiers
head term of a true node
list of arguments
rule id [a list of nodes it applies to]
node id
list of modifiers
head term of a false node
list of arguments
i.e. a rule application that triggers the node
- LangPro & Natural Tableau
- Abzianidze, L., Kogkalidis, K. (2021): A Logic-Based Framework for Natural Language Inference in Dutch. CLIN.
- Abzianidze, L. (2020): Learning as Abduction: Trainable Natural Logic Theorem Prover for Natural Language Inference. *SEM.
- Abzianidze, L. (2017): LangPro: Natural Language Theorem Prover. EMNLP.
- Abzianidze, L. (2016): A Natural Proof System for Natural Language. PhD thesis. Tilburg University.
- Abzianidze, L. (2016): Natural Solution to FraCaS Entailment Problems. *SEM.
- Abzianidze, L. (2015): A Tableau Prover for Natural Logic and Language. EMNLP.
- Abzianidze, L. (2014): Towards a Wide-coverage Tableau Method for Natural Logic. LNAI, Vol. 9067, Springer.
- Muskens, R. (2010): An Analytic Tableau System for Natural Logic. LNCS, Vol. 6042, Springer.
- CCG parsing
- Lewis, M., Steedman, M. (2014): A* CCG Parsing with a Supertag-factored Model. EMNLP.
- Honnibal, M., Curran, J. R., Bos, J. (2010): Rebanking CCGbank for Improved NP Interpretation. ACL (48).
- Clark, S., Curran, J. R. (2007): Wide-Coverage Efficient Statistical Parsing with CCG and Log-Linear Models. Computational Linguistics, 33(4).
- Lexical resources
- Fellbaum, Ch. eds. (1998): WordNet: an Electronic Lexical Database. MIT press.
- Benchmark datasets
- Cooper, R., Crouch, D., Eijck, J. V., Fox, C., Genabith, J. V., Jaspars, J., Kamp, H., Milward, D., Pinkal, M., Poesio, M., Pulman, S., Briscoe, T., Maier, H., and Konrad, K. (1996). FraCaS: A Framework for Computational Semantics. Deliverable D16
- The FraCaS problems converted in xml by B. MacCartney.
- Marelli, M., Menini, S., Baroni, M., Bentivogli, L., Bernardi, R., and Zamparelli, R. (2014b). A sick cure for the evaluation of compositional distributional semantic models. LREC. SICK dataset