Joeun Kim, Seunghyouk Yoon, Xuan-Bach Le, Youngeun Nam, Doyoung Kim, Hwanjun Song, Jae-Gil Lee. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2026.

In the legal field, accurately interpreting and applying legal definitions is crucial yet challenging due to inherent ambiguities. This paper introduces DeCoRA, a novel framework that enhances legal argumentation by incorporating context-based reasoning to address these ambiguities, with a focus on the judge as the central decision maker. Unlike black-box models, such as generative models or outcome prediction systems, which often produce outputs without fully explaining the reasoning behind their conclusions, DeCoRA emphasizes transparency by modeling the judicial decision-making process in a structured and interpretable manner. Our key contributions include: (1) a tree-based knowledge base that organizes legal definitions, highlighting their relationships and effects; (2) a context-aware definition framework enabling judges to interpret definitions considering legal and contextual relevance; and (3) an effective method for handling complex legal scenarios with conflicting or overlapping definitions.

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.

Rely-Guarantee is a comprehensive technique that supports compositional reasoning for concurrent programs. However, specifications of the Rely condition - environment interference, and Guarantee condition - local transformation of thread state - are challenging to establish. Thus the construction of these conditions becomes bottleneck in automating the technique. To tackle the above problem, we propose a verification framework that, based on Rely-Guarantee principles, constructs the correctness proof of concurrent program through inferring suitable Rely -Guarantee conditions automatically. Our framework first constructs a Hoare-style sequential proof for each thread and then applies abstraction refinement to elevate these proofs into concurrent ones with appropriate Rely-Guarantee relations. Experiment results demonstrate that our approach is efficient in proving the correctness of concurrent programs.