Introduction to Natural Tableau and implementation and description of the Natural Tableau-based theorem prover LangPro. Performance of LangPro on the SICK and FraCaS datasets. Using abduction to learn from data.

• L. Abzianidze (2020): Learning as Abduction: Trainable Natural Logic Theorem Prover for Natural Language Inference. Accepted at *SEM.
• L. Abzianidze (2017): LangPro: Natural Language Theorem Prover. EMNLP.
• L. Abzianidze (2016a): Natural Solution to FraCaS Entailment Problems. *SEM.
• L. Abzianidze (2016b): A Natural proof System for Natural Language, PhD thesis, Tilburg University.
• L. Abzianidze (2015): A Tableau Prover for Natural Logic and Language. EMNLP.

Proposal to use a tableau system for natural logic:

• R. Muskens (2010): An Analytic Tableau System for Natural Logic. LNCS, Vol. 6042, Springer.

CCG parsers, EasyCCG and C&C, for English compatible with LangPro:

• M. Lewis & M. Steedman (2014): A* CCG Parsing with a Supertag-factored Model. EMNLP.
• M. Honnibal, J. R. Curran, and J. Bos (2010): Rebanking CCGbank for Improved NP Interpretation. ACL (48).
• S. Clark and J. R. Curran (2007): Wide-Coverage Efficient Statistical Parsing with CCG and Log-Linear Models. Computational Linguistics, 33(4).

WordNet which is used as a lexical knowledge database in the prover:

• Ch. Fellbaum eds. (1998): WordNet: an Electronic Lexical Database. MIT press.

The FraCaS and SICK textual entailment datasets which are use for evaluating the theorem prover:

• 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'14.