@inproceedings{abzianidze-2017-langpro,
    title = "{L}ang{P}ro: Natural Language Theorem Prover",
    author = "Abzianidze, Lasha",
    editor = "Specia, Lucia  and
      Post, Matt  and
      Paul, Michael",
    booktitle = "Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing: System Demonstrations",
    month = sep,
    year = "2017",
    address = "Copenhagen, Denmark",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/iwcs-25-ingestion/D17-2020/",
    doi = "10.18653/v1/D17-2020",
    pages = "115--120",
    abstract = "LangPro is an automated theorem prover for natural language. 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."
}