Natural Language Inference with CCG Parser and Automated Theorem Prover for DTS

Asa Tomita, Mai Matsubara, Hinari Daido, Daisuke Bekki


Abstract
We propose a Natural Language Inference (NLI) system based on compositional semantics. The system combines lightblue, a syntactic and semantic parser grounded in Combinatory Categorial Grammar (CCG) and Dependent Type Semantics (DTS), with wani, an automated theorem prover for Dependent Type Theory (DTT). Because each computational step reflects a theoretical assumption, system evaluation serves as a form of hypothesis verification. We evaluate the inference system using the Japanese Semantic Test Suite JSeM, and demonstrate how error analysis provides feedback to improve both the system and the underlying linguistic theory.
Anthology ID:
2025.brigap-1.1
Volume:
Proceedings of the Second Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-2)
Month:
September
Year:
2025
Address:
Düsseldorf, Germany
Editors:
Timothée Bernard, Timothee Mickus
Venues:
BriGap | WS
SIG:
Publisher:
Association for Computational Linguistics
Note:
Pages:
1–7
Language:
URL:
https://preview.aclanthology.org/iwcs-25-ingestion/2025.brigap-1.1/
DOI:
Bibkey:
Cite (ACL):
Asa Tomita, Mai Matsubara, Hinari Daido, and Daisuke Bekki. 2025. Natural Language Inference with CCG Parser and Automated Theorem Prover for DTS. In Proceedings of the Second Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-2), pages 1–7, Düsseldorf, Germany. Association for Computational Linguistics.
Cite (Informal):
Natural Language Inference with CCG Parser and Automated Theorem Prover for DTS (Tomita et al., BriGap 2025)
Copy Citation:
PDF:
https://preview.aclanthology.org/iwcs-25-ingestion/2025.brigap-1.1.pdf