Acquisition of Phrase Correspondences using Natural Deduction Proofs
How to identify, extract, and use phrasal knowledge is a crucial problem for the task of Recognizing Textual Entailment (RTE). To solve this problem, we propose a method for detecting paraphrases via natural deduction proofs of semantic relations between sentence pairs. Our solution relies on a graph reformulation of partial variable unifications and an algorithm that induces subgraph alignments between meaning representations. Experiments show that our method can automatically detect various paraphrases that are absent from existing paraphrase databases. In addition, the detection of paraphrases using proof information improves the accuracy of RTE tasks.
Code (1)
Tasks
Natural Language InferenceRTESentenceSimilar Papers 제목 키워드 기반
Determining Semantic Textual Similarity using Natural Deduction Proofs
Determining semantic textual similarity is a core research subject in natural language processing. Since vector-based models for sentence representation often use shallow information, capturing accurate semantics is diff…
Semantic Textual SimilaritySentenceFour Geometry Problems to Introduce Automated Deduction in Secondary Schools
The introduction of automated deduction systems in secondary schools face several bottlenecks, the absence of the subject of rigorous mathematical demonstrations in the curricula, the lack of knowledge by the teachers ab…
Chart Parsing Multimodal Grammars
The short note describes the chart parser for multimodal type-logical grammars which has been developed in conjunction with the type-logical treebank for French. The chart parser presents an incomplete but fast implement…
Vocal Bursts Type PredictionHow Deduction Systems Can Help You To Verify Stability Properties
Mathematical proofs are a cornerstone of control theory, and it is important to get them right. Deduction systems can help with this by mechanically checking the proofs. However, the structure and level of detail at whic…
Mathematical ProofsFormalized Lambek Calculus in Higher Order Logic (HOL4)
In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 theorem prover, with some improvements an…