基于ContractCheck的法律合同形式化建模与分析
Formal Modeling and Analysis of Legal Contracts using ContractCheck
摘要：
我们描述了一种方法和工具，称为\textit{ContractCheck}，允许的法律合同，特别是销售采购协议（SPA）的一致性分析。分析依赖于编码的前提执行的条款的SPA，以及建议的一致性约束，使用可判定的片段的一阶逻辑。文本SPA首先以结构化自然语言格式编码，称为块。\textit{ContractCheck}解释这些块和约束，并将它们转换为一阶逻辑断言。然后，它调用可满足性模理论（SMT）求解器，以便通过提供令人满意的模型或通过提供阻碍合同执行的矛盾条款的证据来建立所考虑的合同的可执行性。我们举例说明了\textit{ContractCheck}的应用，并最后提出了未来研究的方向。
英文摘要：
We describe a method and tool called \textit{ContractCheck} that allows for the consistency analysis of legal contracts, in particular Sales Purchase Agreements (SPAs). The analysis relies on an encoding of the premises for the execution of the clauses of an SPA as well as the proposed consistency constraints using decidable fragments of first-order logic. Textual SPAs are first encoded in a structured natural language format, called blocks. \textit{ContractCheck} interprets these blocks and constraints and translates them in first-oder logic assertions. It then invokes a Satisfiability Modulo Theories (SMT) solver in order to establish the executability of a considered contract by either providing a satisfying model, or by providing evidence of contradictory clauses that impede the execution of the contract. We illustrate the application of \textit{ContractCheck} and conclude by proposing directions for future research.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
