@inproceedings{saeki-bekki-2026-execution,
    title = "From Execution to Exploration: Bridging the Usability Gap in Formal Natural Language Inference",
    author = "Saeki, Koharu  and
      Bekki, Daisuke",
    editor = "Bernard, Timoth{\'e}e  and
      Chersoni, Emmanuele  and
      Rambelli, Giulia",
    booktitle = "Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics ({B}ri{G}ap-3)",
    month = jul,
    year = "2026",
    address = "Paris, France",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-brigap/2026.brigap-1.1/",
    pages = "1--11",
    ISBN = "XXX-X-XXXXXX-XX-X",
    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{\texttimes} reduction in debugging turnaround time."
}