We present a system for Natural Language Inference which uses a dynamic semantics converter from abstract syntax trees to Coq types. It combines the fine-grainedness of a dynamic semantics system with the pow-erfulness of a state-of-the-art proof assistant. We evaluate the system on all sections of the FraCaS test suite, excluding section 6. This is the first system that does a complete run on the anaphora and ellipsis sections of the FraCaS. It has a better overall accuracy than any previous system.
展开▼
机译：我们为自然语言推断提供了一个自然语言推断，它使用从抽象语法树到COQ类型的动态语义转换器。它将动态语义系统的细粒度与最先进的证明助手的动态效力相结合。我们在Fracas Test Suite的所有部分评估系统，排除第6节。这是第一个在Fracas的Anaphora和省略号部分上完成的第一个系统。它具有比以前的任何系统更好的整体准确性。
展开▼
