Abstract
Linguistically-oriented formal NLI systems ensure the validity and transparency of inference. However, the combinatorial explosion of candidates, which we term the branching problem, imposes prohibitive computational overhead and a heavy cognitive burden on grammar developers. We argue that a central cause is a mismatch between the exhaustive execution paradigm and the actual workflow of grammar developers. To overcome this barrier, we propose restructuring the development workflow from exhaustive execution to interactive exploration driven by developer decisions. We realize this shift in Express, a web-based interactive development environment for lightblue, a Japanese automated inference system built upon Combinatory Categorial Grammar and Dependent Type Semantics. Express transforms branches at each stage of parsing, type checking, and proof search into explicitly selectable units, transferring control over the reasoning process to the developer. Our evaluation shows that this paradigm shift effectively reduces unnecessary computation and cognitive burden during grammar development: in a user study, we observed a 96% reduction in explored paths and improvement in the task success rate from 25% to 100%. Furthermore, a case study demonstrates a roughly 12× reduction in debugging turnaround time.- Anthology ID:
- 2026.brigap-1.1
- Volume:
[Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3)](/volumes/2026.brigap-1/)- Month:
- July
- Year:
- 2026
- Address:
- Paris, France
- Editors:
[Timothée Bernard](/people/timothee-bernard/),[Emmanuele Chersoni](/people/emmanuele-chersoni/),[Giulia Rambelli](/people/giulia-rambelli/unverified/)- Venues:
[BriGap](/venues/brigap/)|[WS](/venues/ws/)- SIG:
- Publisher:
- Association for Computational Linguistics
- Note:
- Pages:
- 1–11
- Language:
- URL:
[https://aclanthology.org/2026.brigap-1.1/](https://aclanthology.org/2026.brigap-1.1/)- DOI:
- Cite (ACL):
- Koharu Saeki and Daisuke Bekki. 2026. From Execution to Exploration: Bridging the Usability Gap in Formal Natural Language Inference. InProceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3), pages 1–11, Paris, France. Association for Computational Linguistics. - Cite (Informal):
[From Execution to Exploration: Bridging the Usability Gap in Formal Natural Language Inference](https://aclanthology.org/2026.brigap-1.1/)(Saeki & Bekki, BriGap 2026)- PDF:
[https://aclanthology.org/2026.brigap-1.1.pdf](https://aclanthology.org/2026.brigap-1.1.pdf)